1 /-
2 Copyright (c) 2017 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
5 -/
6
7 import topology.continuous_on
src └────────────────────┘
8
9 /-!
10 # Properties of subsets of topological spaces
11
12 ## Main definitions
13
14 `compact`, `is_clopen`, `is_irreducible`, `is_connected`, `is_totally_disconnected`, `is_totally_separated`
15
16 TODO: write better docs
17 -/
18
19 open set filter lattice classical
20 open_locale classical topological_space
21
22 universes u v
23 variables {α : Type u} {β : Type v} [topological_space α]
id ┴ └───────────────┘
src └───────────────┘
typ ┴ └───────────────┘
doc └───────────────┘
24
25 /- compact sets -/
26 section compact
27
28 /-- A set `s` is compact if for every filter `f` that contains `s`,
29 every set of `f` also meets every neighborhood of some `a ∈ s`. -/
30 def compact (s : set α) := ∀f, f ≠ ⊥ → f ≤ principal s → ∃a∈s, f ⊓ 𝓝 a ≠ ⊥
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘ ┴
31
32 lemma compact.inter_right {s t : set α} (hs : compact s) (ht : is_closed t) : compact (s ∩ t) :=
id └─┘ ┴ └─────┘ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ └───────┘ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └───────┘ └─────┘
33 assume f hnf hstf,
id ┴ └─┘ └──┘
typ ┴ └─┘ └──┘
34 let ⟨a, hsa, (ha : f ⊓ 𝓝 a ≠ ⊥)⟩ := hs f hnf (le_trans hstf (le_principal_iff.2 (inter_subset_left _ _))) in
id └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └──────┘ └──┘ └──────────────┘┴ └───────────────┘
src ┴ ┴ ┴ ┴ └──────┘ └──────────────┘┴ └───────────────┘
typ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ └──────┘ └──┘ └──────────────┘┴ └───────────────┘
doc ┴
35 have a ∈ t,
id ┴ ┴
src ┴
typ ┴ ┴
36 from ht.mem_of_nhds_within_ne_bot $ ne_bot_of_le_ne_bot (by { rw inf_comm at ha, exact ha }) $
id └┘└────────────────────────┘ └─────────────────┘ └──────┘ └┘
src └────────────────────────┘ └─────────────────┘ └─┘└──────┘└────┘ └────┘ ┴
typ └┘└────────────────────────┘ └─────────────────┘ └─┘└──────┘└────┘ └────┘└┘┴
doc └─┘ └────┘ └────┘ ┴
txt └─┘ └────┘ └────┘ ┴
par └─┘ └────┘ └────┘ ┴
pid ┴ └────┘ ┴ ┴
st └──────────────────┘└─────────┘└┘
37 inf_le_inf (le_refl _) (le_trans hstf (le_principal_iff.2 (inter_subset_right _ _))),
id └────────┘ └─────┘ └──────┘ └──┘ └──────────────┘┴ └────────────────┘
src └────────┘ └─────┘ └──────┘ └──────────────┘┴ └────────────────┘
typ └────────┘ └─────┘ └──────┘ └──┘ └──────────────┘┴ └────────────────┘
38 ⟨a, ⟨hsa, this⟩, ha⟩
id └──┘
typ └──┘
39
40 lemma compact.inter_left {s t : set α} (ht : compact t) (hs : is_closed s) : compact (s ∩ t) :=
id └─┘ ┴ └─────┘ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ └───────┘ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └───────┘ └─────┘
41 inter_comm t s ▸ ht.inter_right hs
id └────────┘ ┴ ┴ ┴ └┘└──────────┘ └┘
src └────────┘ ┴ └──────────┘
typ └────────┘ ┴ ┴ ┴ └┘└──────────┘ └┘
42
43 lemma compact_diff {s t : set α} (hs : compact s) (ht : is_open t) : compact (s \ t) :=
id └─┘ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ └─────┘ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
44 hs.inter_right (is_closed_compl_iff.mpr ht)
id └┘└──────────┘ └─────────────────┘└──┘ └┘
src └──────────┘ └─────────────────┘└──┘
typ └┘└──────────┘ └─────────────────┘└──┘ └┘
45
46 lemma compact_of_is_closed_subset {s t : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
47 (hs : compact s) (ht : is_closed t) (h : t ⊆ s) : compact t :=
id └─────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
src └─────┘ └───────┘ ┴ └─────┘
typ └─────┘ ┴ └───────┘ ┴ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘ └───────┘ └─────┘
48 inter_eq_self_of_subset_right h ▸ hs.inter_right ht
id └───────────────────────────┘ ┴ ┴ └┘└──────────┘ └┘
src └───────────────────────────┘ ┴ └──────────┘
typ └───────────────────────────┘ ┴ ┴ └┘└──────────┘ └┘
49
50 lemma compact.adherence_nhdset {s t : set α} {f : filter α}
id └─┘ ┴ └────┘ ┴
src └─┘ └────┘
typ └─┘ ┴ └────┘ ┴
51 (hs : compact s) (hf₂ : f ≤ principal s) (ht₁ : is_open t) (ht₂ : ∀a∈s, 𝓝 a ⊓ f ≠ ⊥ → a ∈ t) :
id └─────┘ ┴ ┴ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └───────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ └───────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └───────┘ └─────┘ ┴
52 t ∈ f :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
53 classical.by_cases mem_sets_of_eq_bot $
id └────────────────┘ └────────────────┘
src └────────────────┘ └────────────────┘
typ └────────────────┘ └────────────────┘
54 assume : f ⊓ principal (- t) ≠ ⊥,
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴ ┴
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
55 let ⟨a, ha, (hfa : f ⊓ principal (-t) ⊓ 𝓝 a ≠ ⊥)⟩ := hs _ this $ inf_le_left_of_le hf₂ in
id └─┘ ┴ └┘ ┴ ┴ ┴ └───────┘ ┴┴ ┴ ┴ ┴ ┴ └┘ └──┘ └───────────────┘ └─┘
src ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ └───────────────┘
typ └─┘ ┴ └┘ ┴ ┴ ┴ └───────┘ ┴┴ ┴ ┴ ┴ ┴ └┘ └──┘ └───────────────┘ └─┘
doc └───────┘ ┴
56 have a ∈ t,
id ┴ ┴
src ┴
typ ┴ ┴
57 from ht₂ a ha $ ne_bot_of_le_ne_bot hfa $ le_inf inf_le_right $ inf_le_left_of_le inf_le_left,
id └─┘ └─────────────────┘ └────┘ └──────────┘ └───────────────┘ └─────────┘
src └─────────────────┘ └────┘ └──────────┘ └───────────────┘ └─────────┘
typ └─┘ └─────────────────┘ └────┘ └──────────┘ └───────────────┘ └─────────┘
58 have (-t) ∩ t ∈ nhds_within a (-t),
id ┴┴ ┴ ┴ ┴ └─────────┘ ┴┴
src ┴ ┴ ┴ └─────────┘ ┴
typ ┴┴ ┴ ┴ ┴ └─────────┘ ┴┴
doc └─────────┘
59 from inter_mem_nhds_within _ (mem_nhds_sets ht₁ this),
id └───────────────────┘ └───────────┘ └─┘ └──┘
src └───────────────────┘ └───────────┘
typ └───────────────────┘ └───────────┘ └─┘ └──┘
60 have A : nhds_within a (-t) = ⊥,
id └─────────┘ ┴┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴
typ └─────────┘ ┴┴ ┴ ┴
doc └─────────┘
61 from empty_in_sets_eq_bot.1 $ compl_inter_self t ▸ this,
id └──────────────────┘┴ └──────────────┘ ┴ ┴ └──┘
src └──────────────────┘┴ └──────────────┘ ┴
typ └──────────────────┘┴ └──────────────┘ ┴ ┴ └──┘
62 have nhds_within a (-t) ≠ ⊥,
id └─────────┘ ┴┴ ┴ ┴
src └─────────┘ ┴ ┴ ┴
typ └─────────┘ ┴┴ ┴ ┴
doc └─────────┘
63 from ne_bot_of_le_ne_bot hfa $ le_inf inf_le_right $ inf_le_left_of_le inf_le_right,
id └─────────────────┘ └────┘ └──────────┘ └───────────────┘ └──────────┘
src └─────────────────┘ └────┘ └──────────┘ └───────────────┘ └──────────┘
typ └─────────────────┘ └────┘ └──────────┘ └───────────────┘ └──────────┘
64 absurd A this
id └────┘ ┴ └──┘
src └────┘
typ └────┘ ┴ └──┘
65
66 lemma compact_iff_ultrafilter_le_nhds {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
67 compact s ↔ (∀f, is_ultrafilter f → f ≤ principal s → ∃a∈s, f ≤ 𝓝 a) :=
id └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ └────────────┘ ┴ └───────┘ ┴ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴
doc └─────┘ └────────────┘ └───────┘ ┴
68 ⟨assume hs : compact s, assume f hf hfs,
id └─────┘ ┴ ┴ └┘ └─┘
src └─────┘
typ └─────┘ ┴ ┴ └┘ └─┘
doc └─────┘
69 let ⟨a, ha, h⟩ := hs _ hf.left hfs in
id └─┘ ┴ └┘ ┴ └┘ └┘└───┘ └─┘
src └───┘
typ └─┘ ┴ └┘ ┴ └┘ └┘└───┘ └─┘
70 ⟨a, ha, le_of_ultrafilter hf h⟩,
id └───────────────┘ └┘
src └───────────────┘
typ └───────────────┘ └┘
71
72 assume hs : (∀f, is_ultrafilter f → f ≤ principal s → ∃a∈s, f ≤ 𝓝 a),
id ┴ └────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴
src └────────────┘ ┴ └───────┘ ┴ ┴ ┴ ┴
typ ┴ └────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴
doc └────────────┘ └───────┘ ┴
73 assume f hf hfs,
id ┴ └┘ └─┘
typ ┴ └┘ └─┘
74 let ⟨a, ha, (h : ultrafilter_of f ≤ 𝓝 a)⟩ :=
id └─┘ ┴ └┘ └────────────┘ ┴ ┴ ┴
src └────────────┘ ┴ ┴
typ └─┘ ┴ └┘ └────────────┘ ┴ ┴ ┴
doc └────────────┘ ┴
75 hs (ultrafilter_of f) (ultrafilter_ultrafilter_of hf) (le_trans ultrafilter_of_le hfs) in
id └┘ └────────────┘ ┴ └────────────────────────┘ └┘ └──────┘ └───────────────┘ └─┘
src └────────────┘ └────────────────────────┘ └──────┘ └───────────────┘
typ └┘ └────────────┘ ┴ └────────────────────────┘ └┘ └──────┘ └───────────────┘ └─┘
doc └────────────┘
76 have ultrafilter_of f ⊓ 𝓝 a ≠ ⊥,
id └────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────┘ ┴ ┴ ┴ ┴
typ └────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────┘ ┴
77 by simp only [inf_of_le_left, h]; exact (ultrafilter_ultrafilter_of hf).left,
id └────────────┘ ┴ └────────────────────────┘ └┘
src └─────────┘└────────────┘└┘ ┴ └────┘ └────────────────────────┘┴ └────┘
typ └─────────┘└────────────┘└┘┴┴ └────┘ └────────────────────────┘┴└┘└────┘
doc └─────────┘ └┘ ┴ └────┘ ┴ └────┘
txt └─────────┘ └┘ ┴ └────┘ ┴ └────┘
par └─────────┘ └┘ ┴ └────┘ ┴ └────┘
pid ┴└──┘└┘ └┘ ┴ ┴ ┴ └───┘┴
st └────────────────────────────────────────────────────────────────────────┘
78 ⟨a, ha, ne_bot_of_le_ne_bot this (inf_le_inf ultrafilter_of_le (le_refl _))⟩⟩
id └─────────────────┘ └──┘ └────────┘ └───────────────┘ └─────┘
src └─────────────────┘ └────────┘ └───────────────┘ └─────┘
typ └─────────────────┘ └──┘ └────────┘ └───────────────┘ └─────┘
79
80 lemma compact.elim_finite_subcover {s : set α} {c : set (set α)}
id └─┘ ┴ └─┘ └─┘ ┴
src └─┘ └─┘ └─┘
typ └─┘ ┴ └─┘ └─┘ ┴
81 (hs : compact s) (hc₁ : ∀t∈c, is_open t) (hc₂ : s ⊆ ⋃₀ c) : ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c' :=
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ └┘ └┘
src └─────┘ └─────┘ ┴ └┘ ┴ ┴ └────┘ ┴ ┴ └┘
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ └┘ └┘
doc └─────┘ └─────┘ └────┘
82 classical.by_contradiction $ assume h,
id └────────────────────────┘ ┴
src └────────────────────────┘
typ └────────────────────────┘ ┴
83 have h : ∀{c'}, c' ⊆ c → finite c' → ¬ s ⊆ ⋃₀ c',
id └┘ └┘ ┴ ┴ └────┘ └┘ ┴ ┴ ┴ └┘ └┘
src ┴ └────┘ ┴ ┴ └┘
typ └┘ └┘ ┴ ┴ └────┘ └┘ ┴ ┴ ┴ └┘ └┘
doc └────┘
84 from assume c' h₁ h₂ h₃, h ⟨c', h₁, h₂, h₃⟩,
id └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘
typ └┘ └┘ └┘ └┘ ┴ └┘ └┘ └┘ └┘
85 let
id └─┘
typ └─┘
86 f : filter α := (⨅c':{c' : set (set α) // c' ⊆ c ∧ finite c'}, principal (s - ⋃₀ c')),
id └────┘ ┴ ┴ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └────┘ └┘ ┴ └───────┘ ┴ ┴ └┘ └┘
src └────┘ ┴ ┴ └─┘ └─┘ ┴ ┴ └────┘ ┴ └───────┘ ┴ └┘
typ └────┘ ┴ ┴ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └────┘ └┘ ┴ └───────┘ ┴ ┴ └┘ └┘
doc ┴ └────┘ ┴ └───────┘
87 ⟨a, ha⟩ := (@ne_empty_iff_nonempty α s).1
id ┴ └───────────────────┘ ┴ ┴ ┴
src └───────────────────┘ ┴
typ ┴ └───────────────────┘ ┴ ┴ ┴
88 (assume h', h (empty_subset _) finite_empty $ h'.symm ▸ empty_subset _)
id └┘ ┴ └──────────┘ └──────────┘ └┘└───┘ ┴ └──────────┘
src └──────────┘ └──────────┘ └───┘ ┴ └──────────┘
typ └┘ ┴ └──────────┘ └──────────┘ └┘└───┘ ┴ └──────────┘
89 in
90 have f ≠ ⊥, from infi_ne_bot_of_directed ⟨a⟩
id ┴ ┴ ┴ └─────────────────────┘
src ┴ ┴ └─────────────────────┘
typ ┴ ┴ ┴ └─────────────────────┘
doc └─────────────────────┘
91 (assume ⟨c₁, hc₁, hc'₁⟩ ⟨c₂, hc₂, hc'₂⟩, ⟨⟨c₁ ∪ c₂, union_subset hc₁ hc₂, finite_union hc'₁ hc'₂⟩,
id ┴└┘ └─┘ └──┘ ┴└┘ └─┘ └──┘ ┴ └──────────┘ └──────────┘
src ┴ └──────────┘ └──────────┘
typ ┴└┘ └─┘ └──┘ ┴└┘ └─┘ └──┘ ┴ └──────────┘ └──────────┘
92 principal_mono.mpr $ diff_subset_diff_right $ sUnion_mono $ subset_union_left _ _,
id └────────────┘└──┘ └────────────────────┘ └─────────┘ └───────────────┘
src └────────────┘└──┘ └────────────────────┘ └─────────┘ └───────────────┘
typ └────────────┘└──┘ └────────────────────┘ └─────────┘ └───────────────┘
93 principal_mono.mpr $ diff_subset_diff_right $ sUnion_mono $ subset_union_right _ _⟩)
id └────────────┘└──┘ └────────────────────┘ └─────────┘ └────────────────┘
src └────────────┘└──┘ └────────────────────┘ └─────────┘ └────────────────┘
typ └────────────┘└──┘ └────────────────────┘ └─────────┘ └────────────────┘
94 (assume ⟨c', hc'₁, hc'₂⟩, show principal (s \ _) ≠ ⊥, by simp only [ne.def, principal_eq_bot_iff, diff_eq_empty]; exact h hc'₁ hc'₂),
id ┴ └───────┘ ┴ ┴ ┴ ┴ └────┘ └──────────────────┘ └───────────┘ ┴ └──┘ └──┘
src └───────┘ ┴ ┴ ┴ └─────────┘└────┘└┘└──────────────────┘└┘└───────────┘┴ └────┘ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ ┴ └─────────┘└────┘└┘└──────────────────┘└┘└───────────┘┴ └────┘┴┴└──┘┴└──┘
doc └───────┘ └─────────┘ └┘ └┘ ┴ └────┘ ┴ ┴
txt └─────────┘ └┘ └┘ ┴ └────┘ ┴ ┴
par └─────────┘ └┘ └┘ ┴ └────┘ ┴ ┴
pid ┴└──┘└┘ └┘ └┘ ┴ ┴ ┴ ┴
st └─────────────────────────────────────────────────────────────────────────┘
95 have f ≤ principal s, from infi_le_of_le ⟨∅, empty_subset _, finite_empty⟩ $
id ┴ ┴ └───────┘ ┴ └───────────┘ ┴ └──────────┘ └──────────┘
src ┴ └───────┘ └───────────┘ ┴ └──────────┘ └──────────┘
typ ┴ ┴ └───────┘ ┴ └───────────┘ ┴ └──────────┘ └──────────┘
doc └───────┘
96 show principal (s \ ⋃₀∅) ≤ principal s, from le_principal_iff.2 (diff_subset _ _),
id └───────┘ ┴ ┴ └┘┴ ┴ └───────┘ ┴ └──────────────┘┴ └─────────┘
src └───────┘ ┴ └┘┴ ┴ └───────┘ └──────────────┘┴ └─────────┘
typ └───────┘ ┴ ┴ └┘┴ ┴ └───────┘ ┴ └──────────────┘┴ └─────────┘
doc └───────┘ └───────┘
97 let
id └─┘
typ └─┘
98 ⟨a, ha, (h : f ⊓ 𝓝 a ≠ ⊥)⟩ := hs f ‹f ≠ ⊥› this,
id ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴┴ └──┘
src ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
typ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴┴ ┴ ┴┴ └──┘
doc ┴ ┴ ┴
99 ⟨t, ht₁, (ht₂ : a ∈ t)⟩ := hc₂ ha
id ┴ ┴ └─┘
src ┴
typ ┴ ┴ └─┘
100 in
101 have f ≤ principal (-t),
id ┴ ┴ └───────┘ ┴
src ┴ └───────┘ ┴
typ ┴ ┴ └───────┘ ┴
doc └───────┘
102 from infi_le_of_le ⟨{t}, by rwa singleton_subset_iff, finite_insert _ finite_empty⟩ $
id └───────────┘ ┴ └──────────────────┘ └───────────┘ └──────────┘
src └───────────┘ ┴ └──┘└──────────────────┘ └───────────┘ └──────────┘
typ └───────────┘ ┴ └──┘└──────────────────┘ └───────────┘ └──────────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────────┘
103 principal_mono.mpr $
id └────────────┘└──┘
src └────────────┘└──┘
typ └────────────┘└──┘
104 show s - ⋃₀{t} ⊆ - t, begin rw sUnion_singleton; exact assume x ⟨_, hnt⟩, hnt end,
id ┴ ┴ └┘┴ ┴ ┴ └──────────────┘ └─┘
src ┴ └┘┴ ┴ ┴ └─┘└──────────────┘ └────┘ └─────┘ └─┘ ┴
typ ┴ ┴ └┘┴ ┴ ┴ └─┘└──────────────┘ └────┘ └─────┘└─┘└─┘ ┴
doc └─┘ └────┘ └─────┘ └─┘ ┴
txt └─┘ └────┘ └─────┘ └─┘ ┴
par └─┘ └────┘ └─────┘ └─┘ ┴
pid ┴ ┴ └─────┘ └─┘ ┴
st └──────────────────────────────────────────────────────┘└─┘
105 have is_closed (- t), from is_open_compl_iff.mp $ by rw lattice.neg_neg; exact hc₁ t ht₁,
id └───────┘ ┴ └───────────────┘└─┘ └─────────────┘ └─┘ ┴ └─┘
src └───────┘ ┴ └───────────────┘└─┘ └─┘└─────────────┘ └────┘ ┴ ┴
typ └───────┘ ┴ └───────────────┘└─┘ └─┘└─────────────┘ └────┘└─┘┴┴┴└─┘
doc └───────┘ └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └──────────────────────────────────┘
106 have a ∈ - t, from is_closed_iff_nhds.mp this _ $ ne_bot_of_le_ne_bot h $
id ┴ ┴ └────────────────┘└─┘ └──┘ └─────────────────┘
src ┴ ┴ └────────────────┘└─┘ └─────────────────┘
typ ┴ ┴ └────────────────┘└─┘ └──┘ └─────────────────┘
107 le_inf inf_le_right (inf_le_left_of_le ‹f ≤ principal (- t)›),
id └────┘ └──────────┘ └───────────────┘ ┴┴ ┴ └───────┘ ┴ ┴
src └────┘ └──────────┘ └───────────────┘ ┴ ┴ └───────┘ ┴ ┴
typ └────┘ └──────────┘ └───────────────┘ ┴┴ ┴ └───────┘ ┴ ┴
doc ┴ └───────┘ ┴
108 this ‹a ∈ t›
id └──┘ ┴ ┴ ┴
src ┴ ┴ ┴
typ └──┘ ┴ ┴ ┴
doc ┴ ┴
109
110 lemma compact.elim_finite_subcover_image {s : set α} {b : set β} {c : β → set α}
id └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴
src └─┘ └─┘ └─┘
typ └─┘ ┴ └─┘ ┴ ┴ └─┘ ┴
111 (hs : compact s) (hc₁ : ∀i∈b, is_open (c i)) (hc₂ : s ⊆ ⋃i∈b, c i) :
id └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴ ┴
typ └─────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └─────┘ └─────┘ ┴ ┴
112 ∃b'⊆b, finite b' ∧ s ⊆ ⋃i∈b', c i :=
id ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ ┴┴ └┘┴ ┴ ┴
src ┴ ┴ └────┘ ┴ ┴ ┴ ┴
typ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ ┴┴ └┘┴ ┴ ┴
doc └────┘ ┴ ┴
113 b.eq_empty_or_nonempty.elim (λ h, ⟨∅, empty_subset _, finite_empty, h ▸ hc₂⟩) $
id ┴└───────────────────┘└───┘ ┴ ┴ └──────────┘ └──────────┘ ┴ ┴ └─┘
src └───────────────────┘└───┘ ┴ └──────────┘ └──────────┘ ┴
typ ┴└───────────────────┘└───┘ ┴ ┴ └──────────┘ └──────────┘ ┴ ┴ └─┘
114 assume ⟨i, hi⟩,
id ┴┴
typ ┴┴
115 have hc'₁ : ∀i∈c '' b, is_open i, from assume i ⟨j, hj, h⟩, h ▸ hc₁ _ hj,
id ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘
src └┘ └─────┘ ┴
typ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ └─┘
doc └─────┘
116 have hc'₂ : s ⊆ ⋃₀ (c '' b), by rwa set.sUnion_image,
id ┴ ┴ └┘ ┴ └┘ ┴ └──────────────┘
src ┴ └┘ └┘ └──┘└──────────────┘
typ ┴ ┴ └┘ ┴ └┘ ┴ └──┘└──────────────┘
doc └──┘
txt └──┘
par └──┘
pid ┴
st └───────────────────┘
117 let ⟨d, hd₁, hd₂, hd₃⟩ := hs.elim_finite_subcover hc'₁ hc'₂ in
id └─┘ ┴ └─┘ └─┘ └─┘ └┘└───────────────────┘ └──┘ └──┘
src └───────────────────┘
typ └─┘ ┴ └─┘ └─┘ └─┘ └┘└───────────────────┘ └──┘ └──┘
118 have ∀x : d, ∃i, i ∈ b ∧ c i = x, from assume ⟨x, hx⟩, hd₁ hx,
id ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
119 let ⟨f', hf⟩ := axiom_of_choice this,
id └─┘ └┘ └─────────────┘ └──┘
src └─────────────┘
typ └─┘ └┘ └─────────────┘ └──┘
120 f := λx:set α, (if h : x ∈ d then f' ⟨x, h⟩ else i : β) in
id ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └┘ ┴ ┴
typ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴
121 have ∀(x : α) (i : set α), i ∈ d → x ∈ i → (∃ (i : β), i ∈ f '' d ∧ x ∈ c i),
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
122 from assume x i hid hxi, ⟨f i, mem_image_of_mem f hid,
id ┴ ┴ └─┘ └─┘ ┴ ┴ └──────────────┘ ┴ └─┘
src └──────────────┘
typ ┴ ┴ └─┘ └─┘ ┴ ┴ └──────────────┘ ┴ └─┘
123 by simpa only [f, dif_pos hid, (hf ⟨_, hid⟩).2] using hxi⟩,
id ┴ └─────┘ └─┘ └┘ └─┘ └─┘
src └──────────┘ └┘└─────┘┴ └┘ ┴ └─┘ └──────────┘
typ └──────────┘┴└┘└─────┘┴└─┘└┘ └┘┴ └─┘└─┘└──────────┘└─┘
doc └──────────┘ └┘ ┴ └┘ ┴ └─┘ └──────────┘
txt └──────────┘ └┘ ┴ └┘ ┴ └─┘ └──────────┘
par └──────────┘ └┘ ┴ └┘ ┴ └─┘ └──────────┘
pid ┴└──┘└┘ └┘ ┴ └┘ ┴ └─┘ └───┘┴└────┘
st └─────────────────────────────────────────────────────┘
124 ⟨f '' d,
id ┴ └┘
src └┘
typ ┴ └┘
125 assume i ⟨j, hj, h⟩,
id ┴ ┴ ┴
typ ┴ ┴ ┴
126 h ▸ by simpa only [f, dif_pos hj] using (hf ⟨_, hj⟩).1,
id ┴ ┴ └─────┘ └┘ └┘ └┘
src ┴ └──────────┘ └┘└─────┘┴ └──────┘ ┴ └─┘ └──┘
typ ┴ └──────────┘┴└┘└─────┘┴└┘└──────┘ └┘┴ └─┘└┘└──┘
doc └──────────┘ └┘ ┴ └──────┘ ┴ └─┘ └──┘
txt └──────────┘ └┘ ┴ └──────┘ ┴ └─┘ └──┘
par └──────────┘ └┘ ┴ └──────┘ ┴ └─┘ └──┘
pid ┴└──┘└┘ └┘ ┴ ┴┴└────┘ ┴ └─┘ └┘└┘
st └──────────────────────────────────────────────┘
127 finite_image f hd₂,
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
128 subset.trans hd₃ $ by simpa only [subset_def, mem_sUnion, exists_imp_distrib, mem_Union, exists_prop, and_imp]⟩
id └──────────┘ └────────┘ └────────┘ └────────────────┘ └───────┘ └─────────┘ └─────┘
src └──────────┘ └──────────┘└────────┘└┘└────────┘└┘└────────────────┘└┘└───────┘└┘└─────────┘└┘└─────┘┴
typ └──────────┘ └──────────┘└────────┘└┘└────────┘└┘└────────────────┘└┘└───────┘└┘└─────────┘└┘└─────┘┴
doc └──────────┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └──────────┘ └┘ └┘ └┘ └┘ └┘ ┴
par └──────────┘ └┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ ┴
st └───────────────────────────────────────────────────────────────────────────────────────┘
129
130 section
131 -- this proof times out without this
132 local attribute [instance, priority 1000] classical.prop_decidable
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
133 lemma compact_of_finite_subcover {s : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
134 (h : ∀c, (∀t∈c, is_open t) → s ⊆ ⋃₀ c → ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c') : compact s :=
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ └┘ └┘ └─────┘ ┴
src └─────┘ ┴ └┘ ┴ ┴ └────┘ ┴ ┴ └┘ └─────┘
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ └┘ └┘ └─────┘ ┴
doc └─────┘ └────┘ └─────┘
135 assume f hfn hfs, classical.by_contradiction $ assume : ¬ (∃x∈s, f ⊓ 𝓝 x ≠ ⊥),
id ┴ └─┘ └─┘ └────────────────────────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ └─┘ └────────────────────────┘ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
136 have hf : ∀x∈s, 𝓝 x ⊓ f = ⊥,
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
137 by simpa only [not_exists, not_not, inf_comm],
id └────────┘ └─────┘ └──────┘
src └──────────┘└────────┘└┘└─────┘└┘└──────┘┴
typ └──────────┘└────────┘└┘└─────┘└┘└──────┘┴
doc └──────────┘ └┘ └┘ ┴
txt └──────────┘ └┘ └┘ ┴
par └──────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └─────────────────────────────────────────┘
138 have ¬ ∃x∈s, ∀t∈f.sets, x ∈ closure t,
id ┴ ┴┴ ┴┴ ┴ ┴└───┘ ┴ ┴ └─────┘ ┴
src ┴ ┴ ┴ └───┘ ┴ └─────┘
typ ┴ ┴┴ ┴┴ ┴ ┴└───┘ ┴ ┴ └─────┘ ┴
doc └─────┘
139 from assume ⟨x, hxs, hx⟩,
id ┴┴
typ ┴┴
140 have ∅ ∈ 𝓝 x ⊓ f, by rw [empty_in_sets_eq_bot, hf x hxs],
id ┴ ┴ ┴ ┴ ┴ └──────────────────┘ └┘ ┴ └─┘
src ┴ ┴ ┴ ┴ └──┘└──────────────────┘└┘ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ └──┘└──────────────────┘└┘└┘┴┴┴└─┘┴
doc ┴ └──┘ └┘ ┴ ┴ ┴
txt └──┘ └┘ ┴ ┴ ┴
par └──┘ └┘ ┴ ┴ ┴
pid └┘ └┘ ┴ ┴ ┴
st └───────────────────────┘└────────┘┴
141 let ⟨t₁, ht₁, t₂, ht₂, ht⟩ := by rw [mem_inf_sets] at this; exact this in
id └─┘ └─┘ └┘ └┘ └──────────┘ └──┘
src └──┘└──────────┘└───────┘ └────┘ ┴
typ └─┘ └─┘ └┘ └┘ └──┘└──────────┘└───────┘ └────┘└──┘┴
doc └──┘ └───────┘ └────┘ ┴
txt └──┘ └───────┘ └────┘ ┴
par └──┘ └───────┘ └────┘ ┴
pid └┘ ┴└──────┘ ┴ ┴
st └───────────────┘┴└───────────────────┘
142 have ∅ ∈ 𝓝 x ⊓ principal t₂,
id ┴ ┴ ┴ ┴ └───────┘
src ┴ ┴ ┴ ┴ └───────┘
typ ┴ ┴ ┴ ┴ └───────┘
doc ┴ └───────┘
143 from (𝓝 x ⊓ principal t₂).sets_of_superset (inter_mem_inf_sets ht₁ (subset.refl t₂)) ht,
id ┴ ┴ └───────┘ └──────────────┘ └────────────────┘ └─────────┘
src ┴ ┴ └───────┘ └──────────────┘ └────────────────┘ └─────────┘
typ ┴ ┴ └───────┘ └──────────────┘ └────────────────┘ └─────────┘
doc ┴ └───────┘
144 have 𝓝 x ⊓ principal t₂ = ⊥,
id ┴ ┴ └───────┘ ┴ ┴
src ┴ ┴ └───────┘ ┴ ┴
typ ┴ ┴ └───────┘ ┴ ┴
doc ┴ └───────┘
145 by rwa [empty_in_sets_eq_bot] at this,
id └──────────────────┘
src └───┘└──────────────────┘└───────┘
typ └───┘└──────────────────┘└───────┘
doc └───┘ └───────┘
txt └───┘ └───────┘
par └───┘ └───────┘
pid └┘ ┴└──────┘
st └────────────────────────┘┴└──────┘
146 by simp only [closure_eq_nhds] at hx; exact hx t₂ ht₂ this,
id └─────────────┘ └┘ └┘ └─┘ └──┘
src └─────────┘└─────────────┘└─────┘ └────┘ ┴ ┴ ┴
typ └─────────┘└─────────────┘└─────┘ └────┘└┘┴└┘┴└─┘┴└──┘
doc └─────────┘ └─────┘ └────┘ ┴ ┴ ┴
txt └─────────┘ └─────┘ └────┘ ┴ ┴ ┴
par └─────────┘ └─────┘ └────┘ ┴ ┴ ┴
pid ┴└──┘└┘ ┴┴└───┘ ┴ ┴ ┴ ┴
st └──────────────────────────────────────────────────────┘
147 have ∀x∈s, ∃t∈f.sets, x ∉ closure t, by simpa only [not_exists, not_forall],
id ┴ ┴ ┴┴ ┴└───┘┴ ┴ ┴ └─────┘ ┴ └────────┘ └────────┘
src ┴ └───┘┴ ┴ └─────┘ └──────────┘└────────┘└┘└────────┘┴
typ ┴ ┴ ┴┴ ┴└───┘┴ ┴ ┴ └─────┘ ┴ └──────────┘└────────┘└┘└────────┘┴
doc └─────┘ └──────────┘ └┘ ┴
txt └──────────┘ └┘ ┴
par └──────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └──────────────────────────────────┘
148 let c := (λt, - closure t) '' f.sets, ⟨c', hcc', hcf, hsc'⟩ := h c
id └─┘ ┴ ┴ ┴ └─────┘ ┴ └┘ ┴└───┘ └┘ └──┘ └─┘ └──┘ ┴ ┴
src ┴ └─────┘ └┘ └───┘
typ └─┘ ┴ ┴ ┴ └─────┘ ┴ └┘ ┴└───┘ └┘ └──┘ └─┘ └──┘ ┴ ┴
doc └─────┘
149 (assume t ⟨s, hs, h⟩, h ▸ is_closed_closure) (by simpa only [subset_def, sUnion_image, mem_Union]) in
id ┴ ┴ ┴ ┴ └───────────────┘ └────────┘ └──────────┘ └───────┘
src ┴ └───────────────┘ └──────────┘└────────┘└┘└──────────┘└┘└───────┘┴
typ ┴ ┴ ┴ ┴ └───────────────┘ └──────────┘└────────┘└┘└──────────┘└┘└───────┘┴
doc └──────────┘ └┘ └┘ ┴
txt └──────────┘ └┘ └┘ ┴
par └──────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └───────────────────────────────────────────────┘
150 let ⟨b, hb⟩ := axiom_of_choice $
id └─┘ ┴ └┘ └─────────────┘
src └─────────────┘
typ └─┘ ┴ └┘ └─────────────┘
151 show ∀s:c', ∃t, t ∈ f ∧ - closure t = s,
id ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └─────┘ ┴
typ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘
152 from assume ⟨x, hx⟩, hcc' hx in
id ┴ └┘
typ ┴ └┘
153 have (⋂s∈c', if h : s ∈ c' then b ⟨s, h⟩ else univ) ∈ f,
id ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴ └┘ ┴ └──┘ ┴
typ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc ┴ ┴
154 from Inter_mem_sets hcf $ assume t ht, by rw [dif_pos ht]; exact (hb ⟨t, ht⟩).left,
id └────────────┘ ┴ └┘ └─────┘ └┘ └┘ ┴ └┘
src └────────────┘ └──┘└─────┘┴ ┴ └────┘ ┴ └┘ └─────┘
typ └────────────┘ ┴ └┘ └──┘└─────┘┴└┘┴ └────┘ └┘┴ ┴└┘└┘└─────┘
doc └──┘ ┴ ┴ └────┘ ┴ └┘ └─────┘
txt └──┘ ┴ ┴ └────┘ ┴ └┘ └─────┘
par └──┘ ┴ ┴ └────┘ ┴ └┘ └─────┘
pid └┘ ┴ ┴ ┴ ┴ └┘ └────┘┴
st └─────────────┘┴└───────────────────────┘
155 have s ∩ (⋂s∈c', if h : s ∈ c' then b ⟨s, h⟩ else univ) ∈ f,
id ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ ┴ ┴ └┘ ┴ └──┘ ┴
typ ┴ ┴ ┴┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
doc ┴ ┴
156 from inter_mem_sets (le_principal_iff.1 hfs) this,
id └────────────┘ └──────────────┘┴ └─┘ └──┘
src └────────────┘ └──────────────┘┴
typ └────────────┘ └──────────────┘┴ └─┘ └──┘
157 have ∅ ∈ f,
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
158 from mem_sets_of_superset this $ assume x ⟨hxs, hxi⟩,
id └──────────────────┘ └──┘ ┴ ┴└─┘
src └──────────────────┘
typ └──────────────────┘ └──┘ ┴ ┴└─┘
159 let ⟨t, htc', hxt⟩ := (show ∃t ∈ c', x ∈ t, from hsc' hxs) in
id └─┘ ┴ └──┘ └─┘ ┴┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ └─┘ ┴ └──┘ └─┘ ┴┴ ┴ ┴ ┴ ┴
160 have -closure (b ⟨t, htc'⟩) = t, from (hb _).right,
id ┴└─────┘ ┴ └───┘
src ┴└─────┘ ┴ └───┘
typ ┴└─────┘ ┴ └───┘
doc └─────┘
161 have x ∈ - t,
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
162 from this ▸ (calc x ∈ b ⟨t, htc'⟩ : by rw mem_bInter_iff at hxi; have h := hxi t htc'; rwa [dif_pos htc'] at h
id └──┘ ┴ ┴ └────────────┘ └─┘ ┴ └──┘ └─────┘ └──┘
src ┴ └─┘└────────────┘└─────┘ └────────┘ ┴ ┴ └───┘└─────┘┴ └──────
typ └──┘ ┴ ┴ └─┘└────────────┘└─────┘ └────────┘└─┘┴┴┴└──┘ └───┘└─────┘┴└──┘└──────
doc └─┘ └─────┘ └────────┘ ┴ ┴ └───┘ ┴ └──────
txt └─┘ └─────┘ └────────┘ ┴ ┴ └───┘ ┴ └──────
par └─┘ └─────┘ └────────┘ ┴ ┴ └───┘ ┴ └──────
pid ┴ └─────┘ └────┘┴└─┘ ┴ ┴ └┘ ┴ ┴└───┘└
st └────────────────────────────────────────────────────┘└──────────┘┴└─────
163 ... ⊆ closure (b ⟨t, htc'⟩) : subset_closure
id └─────┘ └────────────┘
src ───────┘ └─────┘ └────────────┘
typ ───────┘ └─────┘ └────────────┘
doc ───────┘ └─────┘
txt ───────┘
par ───────┘
pid ───────┘
st ───────┘
164 ... ⊆ - - closure (b ⟨t, htc'⟩) : by rw lattice.neg_neg; exact subset.refl _),
id ┴ ┴ └─────┘ └─────────────┘ └─────────┘
src ┴ ┴ └─────┘ └─┘└─────────────┘ └────┘└─────────┘└┘
typ ┴ ┴ └─────┘ └─┘└─────────────┘ └────┘└─────────┘└┘
doc └─────┘ └─┘ └────┘ └┘
txt └─┘ └────┘ └┘
par └─┘ └────┘ └┘
pid ┴ ┴ └┘
st └──────────────────────────────────────┘
165 show false, from this hxt,
id └───┘ └──┘
src └───┘
typ └───┘ └──┘
166 hfn $ by rwa [empty_in_sets_eq_bot] at this
id └─┘ └──────────────────┘
src └───┘└──────────────────┘└────────┘
typ └─┘ └───┘└──────────────────┘└────────┘
doc └───┘ └────────┘
txt └───┘ └────────┘
par └───┘ └────────┘
pid └┘ ┴└──────┘┴
st └────────────────────────┘┴└───────┘
167 end
168
169 lemma compact_iff_finite_subcover {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
170 compact s ↔ (∀c, (∀t∈c, is_open t) → s ⊆ ⋃₀ c → ∃c'⊆c, finite c' ∧ s ⊆ ⋃₀ c') :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ └┘ └┘
src └─────┘ ┴ └─────┘ ┴ └┘ ┴ ┴ └────┘ ┴ ┴ └┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ └┘ ┴ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ └┘ └┘
doc └─────┘ └─────┘ └────┘
171 ⟨assume hc c, hc.elim_finite_subcover, compact_of_finite_subcover⟩
id └┘ ┴ └┘└───────────────────┘ └────────────────────────┘
src └───────────────────┘ └────────────────────────┘
typ └┘ ┴ └┘└───────────────────┘ └────────────────────────┘
172
173 @[simp]
doc └──┘
174 lemma compact_empty : compact (∅ : set α) :=
id └─────┘ ┴ └─┘ ┴
src └─────┘ ┴ └─┘
typ └─────┘ ┴ └─┘ ┴
doc └─────┘
175 assume f hnf hsf, not.elim hnf $
id ┴ └─┘ └─┘ └──────┘ └─┘
src └──────┘
typ ┴ └─┘ └─┘ └──────┘ └─┘
176 empty_in_sets_eq_bot.1 $ le_principal_iff.1 hsf
id └──────────────────┘┴ └──────────────┘┴ └─┘
src └──────────────────┘┴ └──────────────┘┴
typ └──────────────────┘┴ └──────────────┘┴ └─┘
177
178 @[simp]
doc └──┘
179 lemma compact_singleton {a : α} : compact ({a} : set α) :=
id ┴ └─────┘ ┴┴ └─┘ ┴
src └─────┘ ┴ └─┘
typ ┴ └─────┘ ┴┴ └─┘ ┴
doc └─────┘
180 compact_of_finite_subcover $ assume c hc₁ hc₂,
id └────────────────────────┘ ┴ └─┘ └─┘
src └────────────────────────┘
typ └────────────────────────┘ ┴ └─┘ └─┘
181 let ⟨i, hic, hai⟩ := (show ∃i ∈ c, a ∈ i, from mem_sUnion.1 $ singleton_subset_iff.1 hc₂) in
id └─┘ ┴ └─┘ ┴┴ ┴┴ ┴ ┴ ┴ └────────┘┴ └──────────────────┘┴ └─┘
src ┴ ┴ ┴ └────────┘┴ └──────────────────┘┴
typ └─┘ ┴ └─┘ ┴┴ ┴┴ ┴ ┴ ┴ └────────┘┴ └──────────────────┘┴ └─┘
182 ⟨{i}, singleton_subset_iff.2 hic, finite_singleton _, by rwa [sUnion_singleton, singleton_subset_iff]⟩
id ┴ └──────────────────┘┴ └──────────────┘ └──────────────┘ └──────────────────┘
src ┴ └──────────────────┘┴ └──────────────┘ └───┘└──────────────┘└┘└──────────────────┘┴
typ ┴ └──────────────────┘┴ └──────────────┘ └───┘└──────────────┘└┘└──────────────────┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st └────────────────────┘└────────────────────┘┴
183
184 lemma set.finite.compact_bUnion {s : set β} {f : β → set α} (hs : finite s) :
id └─┘ ┴ ┴ └─┘ ┴ └────┘ ┴
src └─┘ └─┘ └────┘
typ └─┘ ┴ ┴ └─┘ ┴ └────┘ ┴
doc └────┘
185 (∀i ∈ s, compact (f i)) → compact (⋃i ∈ s, f i) :=
id ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴┴ ┴┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴
typ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴┴ ┴┴ ┴ ┴
doc └─────┘ └─────┘ ┴ ┴
186 assume hf, compact_of_finite_subcover $ assume c c_open c_cover,
id └┘ └────────────────────────┘ ┴ └────┘ └─────┘
src └────────────────────────┘
typ └┘ └────────────────────────┘ ┴ └────┘ └─────┘
187 have ∀i : subtype s, ∃c' ⊆ c, finite c' ∧ f i ⊆ ⋃₀ c', from
id └─────┘ ┴ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ ┴ └┘ └┘
src └─────┘ ┴ ┴ └────┘ ┴ ┴ └┘
typ └─────┘ ┴ ┴└┘ ┴┴ └────┘ └┘ ┴ ┴ ┴ ┴ └┘ └┘
doc └────┘
188 assume ⟨i, hi⟩, (hf i hi).elim_finite_subcover c_open
id ┴┴ └┘ └┘ └──────────────────┘ └────┘
src └──────────────────┘
typ ┴┴ └┘ └┘ └──────────────────┘ └────┘
189 (calc f i ⊆ ⋃i ∈ s, f i : subset_bUnion_of_mem hi
id ┴ ┴┴ ┴┴ ┴ ┴ └──────────────────┘
src ┴ ┴ └──────────────────┘
typ ┴ ┴┴ ┴┴ ┴ ┴ └──────────────────┘
doc ┴ ┴
190 ... ⊆ ⋃₀ c : c_cover),
id └┘ ┴ └─────┘
src └┘
typ └┘ ┴ └─────┘
191 let ⟨finite_subcovers, h⟩ := axiom_of_choice this in
id └─┘ └──────────────┘ ┴ └─────────────┘ └──┘
src └─────────────┘
typ └─┘ └──────────────┘ ┴ └─────────────┘ └──┘
192 let c' := ⋃i, finite_subcovers i in
id └┘ ┴┴┴ ┴
src ┴ ┴
typ └┘ ┴┴┴ ┴
doc ┴ ┴
193 have c' ⊆ c, from Union_subset (λi, (h i).fst),
id └┘ ┴ ┴ └──────────┘ ┴ ┴ └─┘
src ┴ └──────────┘ └─┘
typ └┘ ┴ ┴ └──────────┘ ┴ ┴ └─┘
194 have finite c', from @finite_Union _ _ hs.fintype _ (λi, (h i).snd.1),
id └────┘ └┘ └──────────┘ └┘└──────┘ ┴ ┴ └─┘ ┴
src └────┘ └──────────┘ └──────┘ └─┘ ┴
typ └────┘ └┘ └──────────┘ └┘└──────┘ ┴ ┴ └─┘ ┴
doc └────┘ └──────┘
195 have (⋃i ∈ s, f i) ⊆ ⋃₀ c', from bUnion_subset $ λi hi, calc
id ┴┴ ┴┴ ┴ ┴ ┴ └┘ └┘ └───────────┘ ┴ └┘
src ┴ ┴ ┴ └┘ └───────────┘
typ ┴┴ ┴┴ ┴ ┴ ┴ └┘ └┘ └───────────┘ ┴ └┘
doc ┴ ┴
196 f i ⊆ ⋃₀ finite_subcovers ⟨i,hi⟩ : (h ⟨i,hi⟩).snd.2
id ┴ ┴ └┘ ┴ └┘ ┴ └┘ └─┘ ┴
src └┘ └─┘ ┴
typ ┴ ┴ └┘ ┴ └┘ ┴ └┘ └─┘ ┴
197 ... ⊆ ⋃₀ c' : sUnion_mono (subset_Union _ _),
id └┘ └┘ └─────────┘ └──────────┘
src └┘ └─────────┘ └──────────┘
typ └┘ └┘ └─────────┘ └──────────┘
198 ⟨c', ‹c' ⊆ c›, ‹finite c'›, this⟩
id └┘ ┴└┘ ┴ ┴┴ ┴└────┘ └┘┴ └──┘
src ┴ ┴ ┴ ┴└────┘ ┴
typ └┘ ┴└┘ ┴ ┴┴ ┴└────┘ └┘┴ └──┘
doc ┴ ┴ ┴└────┘ ┴
199
200 lemma compact_Union {f : β → set α} [fintype β]
id ┴ └─┘ ┴ └─────┘ ┴
src └─┘ └─────┘
typ ┴ └─┘ ┴ └─────┘ ┴
doc └─────┘
201 (h : ∀i, compact (f i)) : compact (⋃i, f i) :=
id ┴ └─────┘ ┴ ┴ └─────┘ ┴┴┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ └─────┘ ┴┴┴ ┴ ┴
doc └─────┘ └─────┘ ┴ ┴
202 by rw ← bUnion_univ; exact finite_univ.compact_bUnion (λ i _, h i)
id └─────────┘ └────────────────────────┘ ┴
src └───┘└─────────┘ └────┘└────────────────────────┘┴ └────┘ ┴ └─
typ └───┘└─────────┘ └────┘└────────────────────────┘┴ └────┘┴┴ └─
doc └───┘ └────┘ ┴ └────┘ ┴ └─
txt └───┘ └────┘ ┴ └────┘ ┴ └─
par └───┘ └────┘ ┴ └────┘ ┴ └─
pid └─┘ ┴ ┴ └────┘ ┴ ┴└
st └────────────────────────────────────────────────────────────────
203
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
204 lemma set.finite.compact {s : set α} (hs : finite s) : compact s :=
id └─┘ ┴ └────┘ ┴ └─────┘ ┴
src └─┘ └────┘ └─────┘
typ └─┘ ┴ └────┘ ┴ └─────┘ ┴
doc └────┘ └─────┘
205 bUnion_of_singleton s ▸ hs.compact_bUnion (λ _ _, compact_singleton)
id └─────────────────┘ ┴ ┴ └┘└─────────────┘ ┴ ┴ └───────────────┘
src └─────────────────┘ ┴ └─────────────┘ └───────────────┘
typ └─────────────────┘ ┴ ┴ └┘└─────────────┘ ┴ ┴ └───────────────┘
206
207 lemma compact.union {s t : set α} (hs : compact s) (ht : compact t) : compact (s ∪ t) :=
id └─┘ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
src └─┘ └─────┘ └─────┘ └─────┘ ┴
typ └─┘ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────┘
208 by rw union_eq_Union; exact compact_Union (λ b, by cases b; assumption)
id └────────────┘ └───────────┘ ┴
src └─┘└────────────┘ └────┘└───────────┘┴ └──┘ ┴└────┘ └┘└────────┘└─
typ └─┘└────────────┘ └────┘└───────────┘┴ └──┘ ┴└────┘┴└┘└────────┘└─
doc └─┘ └────┘ ┴ └──┘ ┴└────┘ └┘└────────┘└─
txt └─┘ └────┘ ┴ └──┘ ┴└────┘ └┘└────────┘└─
par └─┘ └────┘ ┴ └──┘ ┴└────┘ └┘└────────┘└─
pid ┴ ┴ ┴ └──┘ └─────┘ └───────────┘└
st └──────────────────────────────────────────────┘└──────────────────┘└─
209
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
210 section tube_lemma
211
212 variables [topological_space β]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
213
214 /-- `nhds_contain_boxes s t` means that any open neighborhood of `s × t` in `α × β` includes
215 a product of an open neighborhood of `s` by an open neighborhood of `t`. -/
216 def nhds_contain_boxes (s : set α) (t : set β) : Prop :=
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
217 ∀ (n : set (α × β)) (hn : is_open n) (hp : set.prod s t ⊆ n),
id └─┘ ┴ ┴ ┴ └─────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─────┘ └──────┘ ┴
typ └─┘ ┴ ┴ ┴ └─────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └─────┘ └──────┘
218 ∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ set.prod u v ⊆ n
id ┴ └─┘ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ └─┘ └─┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
typ ┴ └─┘ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ └──────┘
219
220 lemma nhds_contain_boxes.symm {s : set α} {t : set β} :
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
221 nhds_contain_boxes s t → nhds_contain_boxes t s :=
id └────────────────┘ ┴ ┴ └────────────────┘ ┴ ┴
src └────────────────┘ └────────────────┘
typ └────────────────┘ ┴ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘ └────────────────┘
222 assume H n hn hp,
id ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘
223 let ⟨u, v, uo, vo, su, tv, p⟩ :=
id └─┘ ┴ ┴ └┘ └┘ └┘ └┘
typ └─┘ ┴ ┴ └┘ └┘ └┘ └┘
224 H (prod.swap ⁻¹' n)
id ┴ └───────┘ └─┘ ┴
src └───────┘ └─┘
typ ┴ └───────┘ └─┘ ┴
doc └───────┘ └─┘
225 (continuous_swap n hn)
id └─────────────┘ ┴ └┘
src └─────────────┘
typ └─────────────┘ ┴ └┘
226 (by rwa [←image_subset_iff, prod.swap, image_swap_prod]) in
id └──────────────┘ └───────┘ └─────────────┘
src └────┘└──────────────┘└┘└───────┘└┘└─────────────┘┴
typ └────┘└──────────────┘└┘└───────┘└┘└─────────────┘┴
doc └────┘└──────────────┘└┘└───────┘└┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid └─┘ └┘ └┘ ┴
st └─────────────────────┘└─────────┘└───────────────┘┴
227 ⟨v, u, vo, uo, tv, su,
228 by rwa [←image_subset_iff, prod.swap, image_swap_prod] at p⟩
id └──────────────┘ └───────┘ └─────────────┘
src └────┘└──────────────┘└┘└───────┘└┘└─────────────┘└────┘
typ └────┘└──────────────┘└┘└───────┘└┘└─────────────┘└────┘
doc └────┘└──────────────┘└┘└───────┘└┘ └────┘
txt └────┘ └┘ └┘ └────┘
par └────┘ └┘ └┘ └────┘
pid └─┘ └┘ └┘ ┴└───┘
st └─────────────────────┘└─────────┘└───────────────┘┴└───┘
229
230 lemma nhds_contain_boxes.comm {s : set α} {t : set β} :
id └─┘ ┴ └─┘ ┴
src └─┘ └─┘
typ └─┘ ┴ └─┘ ┴
231 nhds_contain_boxes s t ↔ nhds_contain_boxes t s :=
id └────────────────┘ ┴ ┴ ┴ └────────────────┘ ┴ ┴
src └────────────────┘ ┴ └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘ └────────────────┘
232 iff.intro nhds_contain_boxes.symm nhds_contain_boxes.symm
id └───────┘ └─────────────────────┘ └─────────────────────┘
src └───────┘ └─────────────────────┘ └─────────────────────┘
typ └───────┘ └─────────────────────┘ └─────────────────────┘
233
234 lemma nhds_contain_boxes_of_singleton {x : α} {y : β} :
id ┴ ┴
typ ┴ ┴
235 nhds_contain_boxes ({x} : set α) ({y} : set β) :=
id └────────────────┘ ┴┴ └─┘ ┴ ┴┴ └─┘ ┴
src └────────────────┘ ┴ └─┘ ┴ └─┘
typ └────────────────┘ ┴┴ └─┘ ┴ ┴┴ └─┘ ┴
doc └────────────────┘
236 assume n hn hp,
id ┴ └┘ └┘
typ ┴ └┘ └┘
237 let ⟨u, v, uo, vo, xu, yv, hp'⟩ :=
id └─┘ ┴ ┴ └┘ └┘ └─┘
typ └─┘ ┴ ┴ └┘ └┘ └─┘
238 is_open_prod_iff.mp hn x y (hp $ by simp) in
id └──────────────┘└─┘ └┘ ┴ ┴ └┘
src └──────────────┘└─┘ └──┘
typ └──────────────┘└─┘ └┘ ┴ ┴ └┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
239 ⟨u, v, uo, vo, by simpa, by simpa, hp'⟩
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
st └────┘ └────┘
240
241 lemma nhds_contain_boxes_of_compact {s : set α} (hs : compact s) (t : set β)
id └─┘ ┴ └─────┘ ┴ └─┘ ┴
src └─┘ └─────┘ └─┘
typ └─┘ ┴ └─────┘ ┴ └─┘ ┴
doc └─────┘
242 (H : ∀ x ∈ s, nhds_contain_boxes ({x} : set α) t) : nhds_contain_boxes s t :=
id ┴ ┴ └────────────────┘ ┴┴ └─┘ ┴ ┴ └────────────────┘ ┴ ┴
src └────────────────┘ ┴ └─┘ └────────────────┘
typ ┴ ┴ └────────────────┘ ┴┴ └─┘ ┴ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘ └────────────────┘
243 assume n hn hp,
id ┴ └┘ └┘
typ ┴ └┘ └┘
244 have ∀x : subtype s, ∃uv : set α × set β,
id └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴┴
src └─────┘ ┴ └─┘ ┴ └─┘ ┴
typ └─────┘ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴┴
245 is_open uv.1 ∧ is_open uv.2 ∧ {↑x} ⊆ uv.1 ∧ t ⊆ uv.2 ∧ set.prod uv.1 uv.2 ⊆ n,
id └─────┘ └┘┴ ┴ └─────┘ └┘┴ ┴ ┴┴┴ ┴ └┘┴ ┴ ┴ ┴ └┘┴ ┴ └──────┘ └┘┴ └┘┴ ┴ ┴
src └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
typ └─────┘ └┘┴ ┴ └─────┘ └┘┴ ┴ ┴┴┴ ┴ └┘┴ ┴ ┴ ┴ └┘┴ ┴ └──────┘ └┘┴ └┘┴ ┴ ┴
doc └─────┘ └─────┘ └──────┘
246 from assume ⟨x, hx⟩,
id ┴┴ └┘
typ ┴┴ └┘
247 have set.prod {x} t ⊆ n, from
id └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴ ┴
doc └──────┘
248 subset.trans (prod_mono (by simpa) (subset.refl _)) hp,
id └──────────┘ └───────┘ └─────────┘ └┘
src └──────────┘ └───────┘ └───┘ └─────────┘
typ └──────────┘ └───────┘ └───┘ └─────────┘ └┘
doc └───┘
txt └───┘
par └───┘
st └────┘
249 let ⟨ux,vx,H1⟩ := H x hx n hn this in ⟨⟨ux,vx⟩,H1⟩,
id └─┘ └┘ └┘ └┘ ┴ ┴ └┘ └──┘
typ └─┘ └┘ └┘ └┘ ┴ ┴ └┘ └──┘
250 let ⟨uvs, h⟩ := classical.axiom_of_choice this in
id └─┘ └─┘ ┴ └───────────────────────┘ └──┘
src └───────────────────────┘
typ └─┘ └─┘ ┴ └───────────────────────┘ └──┘
251 have us_cover : s ⊆ ⋃i, (uvs i).1, from
id ┴ ┴ ┴┴┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴┴┴ ┴ ┴
doc ┴ ┴
252 assume x hx, set.subset_Union _ ⟨x,hx⟩ (by simpa using (h ⟨x,hx⟩).2.2.1),
id ┴ └┘ └──────────────┘ ┴ └┘ ┴ ┴ └┘
src └──────────────┘ └──────────┘ ┴ ┴ └──────┘
typ ┴ └┘ └──────────────┘ ┴ └┘ └──────────┘ ┴┴ ┴┴└┘└──────┘
doc └──────────┘ ┴ ┴ └──────┘
txt └──────────┘ ┴ ┴ └──────┘
par └──────────┘ ┴ ┴ └──────┘
pid ┴└────┘ ┴ ┴ └────┘└┘
st └───────────────────────────┘
253 let ⟨s0, _, s0_fin, s0_cover⟩ :=
id └─┘ └┘ └────┘ └──────┘
typ └─┘ └┘ └────┘ └──────┘
254 hs.elim_finite_subcover_image (λi _, (h i).1) $
id └┘└─────────────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────────────┘ ┴
typ └┘└─────────────────────────┘ ┴ ┴ ┴ ┴
255 by rw bUnion_univ; exact us_cover in
id └─────────┘ └──────┘
src └─┘└─────────┘ └────┘ ┴
typ └─┘└─────────┘ └────┘└──────┘┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st └──────────────────────────────┘
256 let u := ⋃(i ∈ s0), (uvs i).1 in
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
257 let v := ⋂(i ∈ s0), (uvs i).2 in
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴ ┴
258 have is_open u, from is_open_bUnion (λi _, (h i).1),
id └─────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
src └─────┘ └────────────┘ ┴
typ └─────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴
doc └─────┘
259 have is_open v, from is_open_bInter s0_fin (λi _, (h i).2.1),
id └─────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └────────────┘ ┴ ┴
typ └─────┘ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘
260 have t ⊆ v, from subset_bInter (λi _, (h i).2.2.2.1),
id ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────────┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
261 have set.prod u v ⊆ n, from assume ⟨x',y'⟩ ⟨hx',hy'⟩,
id └──────┘ ┴ ┴ ┴ ┴ ┴└┘ ┴ └─┘
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴└┘ ┴ └─┘
doc └──────┘
262 have ∃i ∈ s0, x' ∈ (uvs i).1, by simpa using hx',
id ┴┴ ┴ ┴ ┴ ┴ └─┘
src ┴ ┴ ┴ ┴ └──────────┘
typ ┴┴ ┴ ┴ ┴ ┴ └──────────┘└─┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st └──────────────┘
263 let ⟨i,is0,hi⟩ := this in
id └─┘ ┴ └─┘ └┘ └──┘
typ └─┘ ┴ └─┘ └┘ └──┘
264 (h i).2.2.2.2 ⟨hi, (bInter_subset_of_mem is0 : v ⊆ (uvs i).2) hy'⟩,
id ┴ ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ └──────────────────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └──────────────────┘ ┴ ┴ ┴
265 ⟨u, v, ‹is_open u›, ‹is_open v›, s0_cover, ‹t ⊆ v›, ‹set.prod u v ⊆ n›⟩
id ┴ ┴ ┴└─────┘ ┴┴ ┴└─────┘ ┴┴ ┴┴ ┴ ┴┴ ┴└──────┘ ┴ ┴ ┴ ┴┴
src ┴└─────┘ ┴ ┴└─────┘ ┴ ┴ ┴ ┴ ┴└──────┘ ┴ ┴
typ ┴ ┴ ┴└─────┘ ┴┴ ┴└─────┘ ┴┴ ┴┴ ┴ ┴┴ ┴└──────┘ ┴ ┴ ┴ ┴┴
doc ┴└─────┘ ┴ ┴└─────┘ ┴ ┴ ┴ ┴└──────┘ ┴
266
267 lemma generalized_tube_lemma {s : set α} (hs : compact s) {t : set β} (ht : compact t)
id └─┘ ┴ └─────┘ ┴ └─┘ ┴ └─────┘ ┴
src └─┘ └─────┘ └─┘ └─────┘
typ └─┘ ┴ └─────┘ ┴ └─┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
268 {n : set (α × β)} (hn : is_open n) (hp : set.prod s t ⊆ n) :
id └─┘ ┴ ┴ ┴ └─────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─────┘ └──────┘ ┴
typ └─┘ ┴ ┴ ┴ └─────┘ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └─────┘ └──────┘
269 ∃ (u : set α) (v : set β), is_open u ∧ is_open v ∧ s ⊆ u ∧ t ⊆ v ∧ set.prod u v ⊆ n :=
id ┴ └─┘ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ └─┘ └─┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴
typ ┴ └─┘ ┴ └─┘ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ └──────┘
270 have _, from
271 nhds_contain_boxes_of_compact hs t $ assume x _, nhds_contain_boxes.symm $
id └───────────────────────────┘ └┘ ┴ ┴ ┴ └─────────────────────┘
src └───────────────────────────┘ └─────────────────────┘
typ └───────────────────────────┘ └┘ ┴ ┴ ┴ └─────────────────────┘
272 nhds_contain_boxes_of_compact ht {x} $ assume y _, nhds_contain_boxes_of_singleton,
id └───────────────────────────┘ └┘ ┴┴ ┴ ┴ └─────────────────────────────┘
src └───────────────────────────┘ ┴ └─────────────────────────────┘
typ └───────────────────────────┘ └┘ ┴┴ ┴ ┴ └─────────────────────────────┘
273 this n hn hp
id └──┘ ┴ └┘ └┘
typ └──┘ ┴ └┘ └┘
274
275 end tube_lemma
276
277 /-- Type class for compact spaces. Separation is sometimes included in the definition, especially
278 in the French literature, but we do not include it here. -/
279 class compact_space (α : Type*) [topological_space α] : Prop :=
id └───┘ └───────────────┘ ┴
src └───────────────┘
typ └───┘ └───────────────┘ ┴
doc └───────────────┘
280 (compact_univ : compact (univ : set α))
id └─────┘ └──┘ └─┘ ┴
src └─────┘ └──┘ └─┘
typ └─────┘ └──┘ └─┘ ┴
doc └─────┘
281
282 lemma compact_univ [h : compact_space α] : compact (univ : set α) := h.compact_univ
id └───────────┘ ┴ └─────┘ └──┘ └─┘ ┴ ┴└───────────┘
src └───────────┘ └─────┘ └──┘ └─┘ └───────────┘
typ └───────────┘ ┴ └─────┘ └──┘ └─┘ ┴ ┴└───────────┘
doc └───────────┘ └─────┘
283
284 lemma is_closed.compact [compact_space α] {s : set α} (h : is_closed s) :
id └───────────┘ ┴ └─┘ ┴ └───────┘ ┴
src └───────────┘ └─┘ └───────┘
typ └───────────┘ ┴ └─┘ ┴ └───────┘ ┴
doc └───────────┘ └───────┘
285 compact s :=
id └─────┘ ┴
src └─────┘
typ └─────┘ ┴
doc └─────┘
286 compact_of_is_closed_subset compact_univ h (subset_univ _)
id └─────────────────────────┘ └──────────┘ ┴ └─────────┘
src └─────────────────────────┘ └──────────┘ └─────────┘
typ └─────────────────────────┘ └──────────┘ ┴ └─────────┘
287
288 variables [topological_space β]
id └───────────────┘
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
289
290 lemma compact.image_of_continuous_on {s : set α} {f : α → β} (hs : compact s)
id └─┘ ┴ ┴ ┴ └─────┘ ┴
src └─┘ └─────┘
typ └─┘ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
291 (hf : continuous_on f s) : compact (f '' s) :=
id └───────────┘ ┴ ┴ └─────┘ ┴ └┘ ┴
src └───────────┘ └─────┘ └┘
typ └───────────┘ ┴ ┴ └─────┘ ┴ └┘ ┴
doc └───────────┘ └─────┘
292 begin
st └─────
293 intros l lne ls,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
294 have ne_bot : l.comap f ⊓ principal s ≠ ⊥,
id └─────┘ ┴ ┴ └───────┘ ┴ ┴ ┴
src └────────────┘└─────┘┴ ┴┴┴└───────┘┴ ┴┴┴┴
typ └────────────┘└─────┘┴┴┴┴┴└───────┘┴┴┴┴┴┴
doc └────────────┘└─────┘┴ ┴ ┴└───────┘┴ ┴ ┴
txt └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └─────────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────┘└─
295 from comap_inf_principal_ne_bot_of_image_mem lne (le_principal_iff.1 ls),
id └─────────────────────────────────────┘ └─┘ └──────────────┘ └┘
src └───┘└─────────────────────────────────────┘┴ ┴ └──────────────┘└─┘ ┴
typ └───┘└─────────────────────────────────────┘┴└─┘┴ └──────────────┘└─┘└┘┴
doc └───┘ ┴ ┴ └─┘ ┴
txt └───┘ ┴ ┴ └─┘ ┴
par └───┘ ┴ ┴ └─┘ ┴
pid └───┘ ┴ ┴ └─┘ ┴
st ───────────────────────────────────────────────────────────────────────────┘└─
296 rcases hs (l.comap f ⊓ principal s) ne_bot inf_le_right with ⟨a, has, ha⟩,
id └┘ └─────┘ ┴ └───────┘ ┴ └────┘ └──────────┘
src └─────┘ ┴ └─────┘┴ ┴ ┴└───────┘┴ └┘ ┴└──────────┘└────────────────┘
typ └─────┘└┘┴ └─────┘┴┴┴ ┴└───────┘┴┴└┘└────┘┴└──────────┘└────────────────┘
doc └─────┘ ┴ └─────┘┴ ┴ ┴└───────┘┴ └┘ ┴ └────────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────────────────┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────────────────┘
pid ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └────────────────┘
st ──────────────────────────────────────────────────────────────────────────┘└─
297 use [f a, mem_image_of_mem f has],
id ┴ ┴ └──────────────┘ ┴ └─┘
src └───┘ ┴ └┘└──────────────┘┴ ┴ ┴
typ └───┘┴┴┴└┘└──────────────┘┴┴┴└─┘┴
doc └───┘ ┴ └┘ ┴ ┴ ┴
txt └───┘ ┴ └┘ ┴ ┴ ┴
par └───┘ ┴ └┘ ┴ ┴ ┴
pid └┘ ┴ └┘ ┴ ┴ ┴
st ──────────────────────────────────┘└─
298 rw [inf_assoc, @inf_comm _ _ _ (𝓝 a)] at ha,
id └───────┘ └──────┘ ┴ ┴
src └──┘└───────┘└┘ └──────┘└─────┘ ┴┴ └──────┘
typ └──┘└───────┘└┘ └──────┘└─────┘ ┴┴┴└──────┘
doc └──┘ └┘ └─────┘ ┴┴ └──────┘
txt └──┘ └┘ └─────┘ ┴ └──────┘
par └──┘ └┘ └─────┘ ┴ └──────┘
pid └┘ └┘ └─────┘ ┴ └┘└────┘
st ──────────────┘└─────────────────────┘┴└────┘└─
299 exact ne_bot_of_le_ne_bot (@@map_ne_bot f ha) (tendsto_comap.inf $ hf a has)
id └─────────────────┘ └────────┘ ┴ └┘ └───────────────┘ └┘ ┴ └─┘
src └────┘└─────────────────┘┴ └────────┘┴ ┴ └┘ └───────────────┘┴ ┴ ┴ ┴ └┘
typ └────┘└─────────────────┘┴ └────────┘┴┴┴└┘└┘ └───────────────┘┴ ┴└┘┴┴┴└─┘└┘
doc └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────────┘
300 end
st └─┘
301
302 lemma compact.image {s : set α} {f : α → β} (hs : compact s) (hf : continuous f) :
id └─┘ ┴ ┴ ┴ └─────┘ ┴ └────────┘ ┴
src └─┘ └─────┘ └────────┘
typ └─┘ ┴ ┴ ┴ └─────┘ ┴ └────────┘ ┴
doc └─────┘ └────────┘
303 compact (f '' s) :=
id └─────┘ ┴ └┘ ┴
src └─────┘ └┘
typ └─────┘ ┴ └┘ ┴
doc └─────┘
304 hs.image_of_continuous_on hf.continuous_on
id └┘└─────────────────────┘ └┘└────────────┘
src └─────────────────────┘ └────────────┘
typ └┘└─────────────────────┘ └┘└────────────┘
305
306 lemma compact_range [compact_space α] {f : α → β} (hf : continuous f) :
id └───────────┘ ┴ ┴ ┴ └────────┘ ┴
src └───────────┘ └────────┘
typ └───────────┘ ┴ ┴ ┴ └────────┘ ┴
doc └───────────┘ └────────┘
307 compact (range f) :=
id └─────┘ └───┘ ┴
src └─────┘ └───┘
typ └─────┘ └───┘ ┴
doc └─────┘ └───┘
308 by rw ← image_univ; exact compact_univ.image hf
id └────────┘ └────────────────┘ └┘
src └───┘└────────┘ └────┘└────────────────┘┴ └
typ └───┘└────────┘ └────┘└────────────────┘┴└┘└
doc └───┘ └────┘ ┴ └
txt └───┘ └────┘ ┴ └
par └───┘ └────┘ ┴ └
pid └─┘ ┴ ┴ └
st └─────────────────────────────────────────────
309
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
310 lemma embedding.compact_iff_compact_image {s : set α} {f : α → β} (hf : embedding f) :
id └─┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ └───────┘
typ └─┘ ┴ ┴ ┴ └───────┘ ┴
doc └───────┘
311 compact s ↔ compact (f '' s) :=
id └─────┘ ┴ ┴ └─────┘ ┴ └┘ ┴
src └─────┘ ┴ └─────┘ └┘
typ └─────┘ ┴ ┴ └─────┘ ┴ └┘ ┴
doc └─────┘ └─────┘
312 iff.intro (assume h, h.image hf.continuous) $ assume h, begin
id └───────┘ ┴ ┴└────┘ └┘└─────────┘ ┴
src └───────┘ └────┘ └─────────┘
typ └───────┘ ┴ ┴└────┘ └┘└─────────┘ ┴
st └─────
313 rw compact_iff_ultrafilter_le_nhds at ⊢ h,
id └─────────────────────────────┘
src └─┘└─────────────────────────────┘└─────┘
typ └─┘└─────────────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ──────────────────────────────────────────┘└─
314 intros u hu us',
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
315 let u' : filter β := map f u,
id └────┘ ┴ └─┘ ┴ ┴
src └───────┘└────┘┴ └──┘└─┘┴ ┴
typ └───────┘└────┘┴┴└──┘└─┘┴┴┴┴
doc └───────┘ ┴ └──┘└─┘┴ ┴
txt └───────┘ ┴ └──┘ ┴ ┴
par └───────┘ ┴ └──┘ ┴ ┴
pid └────┘└─┘ ┴ └──┘ ┴ ┴
st ─────────────────────────────┘└─
316 have : u' ≤ principal (f '' s), begin
id └┘ ┴ └───────┘ ┴ └┘ ┴
src └─────┘ ┴┴┴└───────┘┴ ┴└┘┴ ┴
typ └─────┘└┘┴┴┴└───────┘┴ ┴┴└┘┴┴┴
doc └─────┘ ┴ ┴└───────┘┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────┘└─────┘└
317 rw [map_le_iff_le_comap, comap_principal], convert us',
id └─────────────────┘ └─────────────┘ └─┘
src └──┘└─────────────────┘└┘└─────────────┘┴ └──────┘
typ └──┘└─────────────────┘└┘└─────────────┘┴ └──────┘└─┘
doc └──┘ └┘ ┴ └──────┘
txt └──┘ └┘ ┴ └──────┘
par └──┘ └┘ ┴ └──────┘
pid └┘ └┘ ┴ ┴
st ──────────────────────────┘└───────────────┘└────────────┘└─
318 exact preimage_image_eq _ hf.inj
id └───────────────┘ └────┘
src └────┘└───────────────┘└─┘└────┘└
typ └────┘└───────────────┘└─┘└────┘└
doc └────┘ └─┘ └
txt └────┘ └─┘ └
par └────┘ └─┘ └
pid ┴ └─┘ └
st ─────────────────────────────────────
319 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘└─
320 rcases h u' (ultrafilter_map hu) this with ⟨_, ⟨a, ha, ⟨⟩⟩, _⟩,
id ┴ └┘ └─────────────┘ └┘ └──┘
src └─────┘ ┴ ┴ └─────────────┘┴ └┘ └───────────────────────┘
typ └─────┘┴┴└┘┴ └─────────────┘┴└┘└┘└──┘└───────────────────────┘
doc └─────┘ ┴ ┴ ┴ └┘ └───────────────────────┘
txt └─────┘ ┴ ┴ ┴ └┘ └───────────────────────┘
par └─────┘ ┴ ┴ ┴ └┘ └───────────────────────┘
pid ┴ ┴ ┴ ┴ └┘ └───────────────────────┘
st ───────────────────────────────────────────────────────────────┘└─
321 refine ⟨a, ha, _⟩,
id ┴ └┘
src └─────┘ └┘ └──┘
typ └─────┘ ┴└┘└┘└──┘
doc └─────┘ └┘ └──┘
txt └─────┘ └┘ └──┘
par └─────┘ └┘ └──┘
pid ┴ └┘ └──┘
st ──────────────────┘└─
322 rwa [hf.induced, nhds_induced, ←map_le_iff_le_comap]
id └──────────┘ └─────────────────┘
src └───┘ └┘└──────────┘└─┘└─────────────────┘└┘
typ └───┘└────────┘└┘└──────────┘└─┘└─────────────────┘└┘
doc └───┘ └┘ └─┘ └┘
txt └───┘ └┘ └─┘ └┘
par └───┘ └┘ └─┘ └┘
pid └┘ └┘ └─┘ ┴┴
st ────────────────┘└────────────┘└────────────────────┘┴┴
323 end
st └─┘
324
325 lemma compact_iff_compact_in_subtype {p : α → Prop} {s : set {a // p a}} :
id ┴ └─┘ ┴┴ ┴ ┴
src └─┘ ┴
typ ┴ └─┘ ┴┴ ┴ ┴
326 compact s ↔ compact (subtype.val '' s) :=
id └─────┘ ┴ ┴ └─────┘ └─────────┘ └┘ ┴
src └─────┘ ┴ └─────┘ └─────────┘ └┘
typ └─────┘ ┴ ┴ └─────┘ └─────────┘ └┘ ┴
doc └─────┘ └─────┘
327 embedding_subtype_val.compact_iff_compact_image
id └───────────────────┘└────────────────────────┘
src └───────────────────┘└────────────────────────┘
typ └───────────────────┘└────────────────────────┘
328
329 lemma compact_iff_compact_univ {s : set α} : compact s ↔ compact (univ : set (subtype s)) :=
id └─┘ ┴ └─────┘ ┴ ┴ └─────┘ └──┘ └─┘ └─────┘ ┴
src └─┘ └─────┘ ┴ └─────┘ └──┘ └─┘ └─────┘
typ └─┘ ┴ └─────┘ ┴ ┴ └─────┘ └──┘ └─┘ └─────┘ ┴
doc └─────┘ └─────┘
330 by rw [compact_iff_compact_in_subtype, image_univ, subtype.val_range]; refl
id └────────────────────────────┘ └────────┘ └───────────────┘
src └──┘└────────────────────────────┘└┘└────────┘└┘└───────────────┘┴ └────
typ └──┘└────────────────────────────┘└┘└────────┘└┘└───────────────┘┴ └────
doc └──┘ └┘ └┘ ┴ └────
txt └──┘ └┘ └┘ ┴ └────
par └──┘ └┘ └┘ ┴ └────
pid └┘ └┘ └┘ ┴ └
st └─────────────────────────────────┘└──────────┘└─────────────────┘┴└──────
331
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
332 lemma compact_iff_compact_space {s : set α} : compact s ↔ compact_space s :=
id └─┘ ┴ └─────┘ ┴ ┴ └───────────┘ ┴
src └─┘ └─────┘ ┴ └───────────┘
typ └─┘ ┴ └─────┘ ┴ ┴ └───────────┘ ┴
doc └─────┘ └───────────┘
333 compact_iff_compact_univ.trans ⟨λ h, ⟨h⟩, @compact_space.compact_univ _ _⟩
id └──────────────────────┘└────┘ ┴ ┴ └────────────────────────┘
src └──────────────────────┘└────┘ └────────────────────────┘
typ └──────────────────────┘└────┘ ┴ ┴ └────────────────────────┘
334
335 lemma compact.prod {s : set α} {t : set β} (hs : compact s) (ht : compact t) : compact (set.prod s t) :=
id └─┘ ┴ └─┘ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ └──────┘ ┴ ┴
src └─┘ └─┘ └─────┘ └─────┘ └─────┘ └──────┘
typ └─┘ ┴ └─┘ ┴ └─────┘ ┴ └─────┘ ┴ └─────┘ └──────┘ ┴ ┴
doc └─────┘ └─────┘ └─────┘ └──────┘
336 begin
st └─────
337 rw compact_iff_ultrafilter_le_nhds at hs ht ⊢,
id └─────────────────────────────┘
src └─┘└─────────────────────────────┘└─────────┘
typ └─┘└─────────────────────────────┘└─────────┘
doc └─┘ └─────────┘
txt └─┘ └─────────┘
par └─┘ └─────────┘
pid ┴ └─────────┘
st ──────────────────────────────────────────────┘└─
338 intros f hf hfs,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
339 rw le_principal_iff at hfs,
id └──────────────┘
src └─┘└──────────────┘└─────┘
typ └─┘└──────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───────────────────────────┘└─
340 rcases hs (map prod.fst f) (ultrafilter_map hf)
id └┘ └─┘ └──────┘ ┴ └─────────────┘ └┘
src └─────┘ ┴ └─┘┴└──────┘┴ └┘ └─────────────┘┴ └─
typ └─────┘└┘┴ └─┘┴└──────┘┴┴└┘ └─────────────┘┴└┘└─
doc └─────┘ ┴ └─┘┴ ┴ └┘ ┴ └─
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─
pid ┴ ┴ ┴ ┴ └┘ ┴ └─
st ──────────────────────────────────────────────────
341 (le_principal_iff.2 (mem_map_sets_iff.2
id └──────────────┘ └──────────────┘
src ───┘ └──────────────┘└─┘ └──────────────┘└──
typ ───┘ └──────────────┘└─┘ └──────────────┘└──
doc ───┘ └─┘ └──
txt ───┘ └─┘ └──
par ───┘ └─┘ └──
pid ───┘ └─┘ └──
st ────────────────────────────────────────────
342 ⟨_, hfs, image_subset_iff.2 (λ s h, h.1)⟩)) with ⟨a, sa, ha⟩,
id └─┘ └──────────────┘
src ─────┘ └─┘ └┘└──────────────┘└─┘ └────┘ └─────────────────────┘
typ ─────┘ └─┘└─┘└┘└──────────────┘└─┘ └────┘ └─────────────────────┘
doc ─────┘ └─┘ └┘└──────────────┘└─┘ └────┘ └─────────────────────┘
txt ─────┘ └─┘ └┘ └─┘ └────┘ └─────────────────────┘
par ─────┘ └─┘ └┘ └─┘ └────┘ └─────────────────────┘
pid ─────┘ └─┘ └┘ └─┘ └────┘ └─────────────────────┘
st ─────────────────────────────────────────────────────────────────┘└─
343 rcases ht (map prod.snd f) (ultrafilter_map hf)
id └┘ └─┘ └──────┘ ┴ └─────────────┘ └┘
src └─────┘ ┴ └─┘┴└──────┘┴ └┘ └─────────────┘┴ └─
typ └─────┘└┘┴ └─┘┴└──────┘┴┴└┘ └─────────────┘┴└┘└─
doc └─────┘ ┴ └─┘┴ ┴ └┘ ┴ └─
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─
pid ┴ ┴ ┴ ┴ └┘ ┴ └─
st ──────────────────────────────────────────────────
344 (le_principal_iff.2 (mem_map_sets_iff.2
id └──────────────┘ └──────────────┘
src ───┘ └──────────────┘└─┘ └──────────────┘└──
typ ───┘ └──────────────┘└─┘ └──────────────┘└──
doc ───┘ └─┘ └──
txt ───┘ └─┘ └──
par ───┘ └─┘ └──
pid ───┘ └─┘ └──
st ────────────────────────────────────────────
345 ⟨_, hfs, image_subset_iff.2 (λ s h, h.2)⟩)) with ⟨b, tb, hb⟩,
id └─┘ └──────────────┘
src ─────┘ └─┘ └┘└──────────────┘└─┘ └────┘ └─────────────────────┘
typ ─────┘ └─┘└─┘└┘└──────────────┘└─┘ └────┘ └─────────────────────┘
doc ─────┘ └─┘ └┘└──────────────┘└─┘ └────┘ └─────────────────────┘
txt ─────┘ └─┘ └┘ └─┘ └────┘ └─────────────────────┘
par ─────┘ └─┘ └┘ └─┘ └────┘ └─────────────────────┘
pid ─────┘ └─┘ └┘ └─┘ └────┘ └─────────────────────┘
st ─────────────────────────────────────────────────────────────────┘└─
346 rw map_le_iff_le_comap at ha hb,
id └─────────────────┘
src └─┘└─────────────────┘└───────┘
typ └─┘└─────────────────┘└───────┘
doc └─┘ └───────┘
txt └─┘ └───────┘
par └─┘ └───────┘
pid ┴ └───────┘
st ────────────────────────────────┘└─
347 refine ⟨⟨a, b⟩, ⟨sa, tb⟩, _⟩,
id ┴ ┴ └┘ └┘
src └─────┘ └┘ └─┘ └┘ └───┘
typ └─────┘ ┴└┘┴└─┘ └┘└┘└┘└───┘
doc └─────┘ └┘ └─┘ └┘ └───┘
txt └─────┘ └┘ └─┘ └┘ └───┘
par └─────┘ └┘ └─┘ └┘ └───┘
pid ┴ └┘ └─┘ └┘ └───┘
st ─────────────────────────────┘└─
348 rw nhds_prod_eq, exact le_inf ha hb
id └──────────┘ └────┘ └┘ └┘
src └─┘└──────────┘ └────┘└────┘┴ ┴ ┴
typ └─┘└──────────┘ └────┘└────┘┴└┘┴└┘┴
doc └─┘ └────┘ ┴ ┴ ┴
txt └─┘ └────┘ ┴ ┴ ┴
par └─┘ └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ────────────────┘└───────────────────┘
349 end
st └─┘
350
351 /-- Finite topological spaces are compact. -/
352 @[priority 100] instance fintype.compact_space [fintype α] : compact_space α :=
id └─────┘ ┴ └───────────┘ ┴
src └─────┘ └───────────┘
typ └─────┘ ┴ └───────────┘ ┴
doc └─────┘ └───────────┘
353 { compact_univ := set.finite_univ.compact }
id └─────────────┘└──────┘
src └─────────────┘└──────┘
typ └─────────────┘└──────┘
354
355 /-- The product of two compact spaces is compact. -/
356 instance [compact_space α] [compact_space β] : compact_space (α × β) :=
id └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────┘ └───────────┘
357 ⟨by { rw ← univ_prod_univ, exact compact_univ.prod compact_univ }⟩
id └────────────┘ └───────────────┘ └──────────┘
src └───┘└────────────┘ └────┘└───────────────┘┴└──────────┘┴
typ └───┘└────────────┘ └────┘└───────────────┘┴└──────────┘┴
doc └───┘ └────┘ ┴ ┴
txt └───┘ └────┘ ┴ ┴
par └───┘ └────┘ ┴ ┴
pid └─┘ ┴ ┴ ┴
st └────────────────────┘└─────────────────────────────────────┘└┘
358
359 /-- The disjoint union of two compact spaces is compact. -/
360 instance [compact_space α] [compact_space β] : compact_space (α ⊕ β) :=
id └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ └───────────┘ └───────────┘ ┴
typ └───────────┘ ┴ └───────────┘ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────┘ └───────────┘
361 ⟨begin
st └─────
362 rw ← range_inl_union_range_inr,
id └───────────────────────┘
src └───┘└───────────────────────┘
typ └───┘└───────────────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ───────────────────────────────┘└─
363 exact (compact_range continuous_inl).union (compact_range continuous_inr)
id └────────────┘ └───────────┘ └────────────┘
src └────┘ ┴└────────────┘└──────┘ └───────────┘┴└────────────┘└┘
typ └────┘ ┴└────────────┘└──────┘ └───────────┘┴└────────────┘└┘
doc └────┘ ┴ └──────┘ ┴ └┘
txt └────┘ ┴ └──────┘ ┴ └┘
par └────┘ ┴ └──────┘ ┴ └┘
pid ┴ ┴ └──────┘ ┴ ┴┴
st ───────────────────────────────────────────────────────────────────────────┘
364 end⟩
st └─┘
365
366 section tychonoff
367 variables {ι : Type*} {π : ι → Type*} [∀i, topological_space (π i)]
id ┴ ┴ └───────────────┘ ┴
src └───────────────┘
typ ┴ ┴ └───────────────┘ ┴
doc └───────────────┘
368
369 /-- Tychonoff's theorem -/
370 lemma compact_pi_infinite {s : Πi:ι, set (π i)} :
id ┴ └─┘ ┴ ┴
src └─┘
typ ┴ └─┘ ┴ ┴
371 (∀i, compact (s i)) → compact {x : Πi:ι, π i | ∀i, x i ∈ s i} :=
id ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴
typ ┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
372 begin
st └─────
373 simp [compact_iff_ultrafilter_le_nhds, nhds_pi],
id └─────────────────────────────┘ └─────┘
src └────┘└─────────────────────────────┘└┘└─────┘┴
typ └────┘└─────────────────────────────┘└┘└─────┘┴
doc └────┘ └┘ ┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st ────────────────────────────────────────────────┘└─
374 exact assume h f hf hfs,
src └────┘ └────────────
typ └────┘ └────────────
doc └────┘ └────────────
txt └────┘ └────────────
par └────┘ └────────────
pid ┴ └────────────
st ───────────────────────────
375 let p : Πi:ι, filter (π i) := λi, map (λx:Πi:ι, π i, x i) f in
id └────┘ └─┘
src ───┘ └───┘ └┘ ┴└────┘┴ ┴ └───┘ └─┘└─┘┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └───
typ ───┘ └───┘ └┘ ┴└────┘┴ ┴ └───┘ └─┘└─┘┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └───
doc ───┘ └───┘ └┘ ┴ ┴ ┴ └───┘ └─┘└─┘┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └───
txt ───┘ └───┘ └┘ ┴ ┴ ┴ └───┘ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └───
par ───┘ └───┘ └┘ ┴ ┴ ┴ └───┘ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └───
pid ───┘ └───┘ └┘ ┴ ┴ ┴ └───┘ └─┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ └───
st ───────────────────────────────────────────────────────────────────
376 have ∀i:ι, ∃a, a∈s i ∧ p i ≤ 𝓝 a,
id ┴ ┴ ┴ ┴ ┴
src ───┘ ┴ └┘ ┴┴┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴┴ └─
typ ───┘ ┴ └┘ ┴┴┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴┴┴ └─
doc ───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴┴ └─
txt ───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ───┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ──────────────────────────────────────
377 from assume i, h i (p i) (ultrafilter_map hf) $
id └─────────────┘
src ──────────┘ └──┘ ┴ ┴ ┴ └┘ └─────────────┘┴ └┘ └
typ ──────────┘ └──┘ ┴ ┴ ┴ └┘ └─────────────┘┴ └┘ └
doc ──────────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ └
txt ──────────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ └
par ──────────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ └
pid ──────────┘ └──┘ ┴ ┴ ┴ └┘ ┴ └┘ └
st ──────────────────────────────────────────────────────
378 show (λx:Πi:ι, π i, x i) ⁻¹' s i ∈ f.sets,
id ┴ ┴ └─┘ ┴ └───┘
src ─────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘└─┘┴ ┴ ┴ ┴ └───┘└─
typ ─────┘ ┴ └┘ └┘┴ ┴┴┴ └┘ ┴ └┘└─┘┴ ┴ ┴┴┴ └───┘└─
doc ─────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘└─┘┴ ┴ ┴ ┴ └─
txt ─────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └─
par ─────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └─
pid ─────┘ ┴ └┘ └┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────
379 from mem_sets_of_superset hfs $ assume x (hx : ∀i, x i ∈ s i), hx i,
id └──────────────────┘ ┴
src ────────────┘└──────────────────┘┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─
typ ────────────┘└──────────────────┘┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴┴┴ └─┘ ┴ └─
doc ────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─
txt ────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─
par ────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─
pid ────────────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ └─
st ─────────────────────────────────────────────────────────────────────────────
380 let ⟨a, ha⟩ := classical.axiom_of_choice this in
id ┴ └┘ └───────────────────────┘
src ───┘ ┴ └┘ └───┘└───────────────────────┘┴ └───
typ ───┘ ┴ ┴└┘└┘└───┘└───────────────────────┘┴ └───
doc ───┘ ┴ └┘ └───┘ ┴ └───
txt ───┘ ┴ └┘ └───┘ ┴ └───
par ───┘ ┴ └┘ └───┘ ┴ └───
pid ───┘ ┴ └┘ └───┘ ┴ └───
st ─────────────────────────────────────────────────────
381 ⟨a, assume i, (ha i).left, assume i, map_le_iff_le_comap.mp $ (ha i).right⟩
id └────────────────────┘
src ───┘ └┘ └──┘ ┴ └──────┘ └──┘└────────────────────┘┴ ┴ ┴ └───────┘
typ ───┘ └┘ └──┘ ┴ └──────┘ └──┘└────────────────────┘┴ ┴ ┴ └───────┘
doc ───┘ └┘ └──┘ ┴ └──────┘ └──┘ ┴ ┴ ┴ └───────┘
txt ───┘ └┘ └──┘ ┴ └──────┘ └──┘ ┴ ┴ ┴ └───────┘
par ───┘ └┘ └──┘ ┴ └──────┘ └──┘ ┴ ┴ ┴ └───────┘
pid ───┘ └┘ └──┘ ┴ └──────┘ └──┘ ┴ ┴ ┴ └──────┘┴
st ───────────────────────────────────────────────────────────────────────────────┘
382 end
st └─┘
383
384 instance pi.compact [∀i:ι, compact_space (π i)] : compact_space (Πi, π i) :=
id ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───────────┘ └───────────┘
typ ┴ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └───────────┘ └───────────┘
385 ⟨begin
st └─────
386 have A : compact {x : Πi:ι, π i | ∀i, x i ∈ (univ : set (π i))} :=
id └─────┘ ┴ ┴ ┴ └──┘ └─┘ ┴
src └───────┘└─────┘┴┴└──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴┴ └──┘└─┘└─┘┴ ┴ └──────
typ └───────┘└─────┘┴┴└──┘ └┘┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴┴ └──┘└─┘└─┘┴ ┴┴ └──────
doc └───────┘└─────┘┴ └──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────
txt └───────┘ ┴ └──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────
par └───────┘ ┴ └──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──────
pid └────┘└─┘ ┴ └──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘└───
st ─────────────────────────────────────────────────────────────────────
387 compact_pi_infinite (λi, compact_univ),
id └─────────────────┘ └──────────┘
src ───┘└─────────────────┘┴ └─┘└──────────┘┴
typ ───┘└─────────────────┘┴ └─┘└──────────┘┴
doc ───┘└─────────────────┘┴ └─┘ ┴
txt ───┘ ┴ └─┘ ┴
par ───┘ ┴ └─┘ ┴
pid ───┘ ┴ └─┘ ┴
st ─────────────────────────────────────────┘└─
388 have : {x : Πi:ι, π i | ∀i, x i ∈ (univ : set (π i))} = univ := by ext; simp,
id ┴ ┴ └─┘ ┴ ┴ └──┘
src └─────┘┴└──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘└─┘┴ ┴ └──┘┴┴└──┘└──┘ ┴└─┘└┘└──┘
typ └─────┘┴└──┘ └┘┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘└─┘┴ ┴┴ └──┘┴┴└──┘└──┘ ┴└─┘└┘└──┘
doc └─────┘ └──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ ┴└─┘└┘└──┘
txt └─────┘ └──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ ┴└─┘└┘└──┘
par └─────┘ └──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ ┴└─┘└┘└──┘
pid └───┘└┘ └──┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘ ┴ └──┘ └────────┘
st ───────────────────────────────────────────────────────────────────┘└────────┘└─
389 rwa this at A,
id └──┘
src └──┘ └───┘
typ └──┘└──┘└───┘
doc └──┘ └───┘
txt └──┘ └───┘
par └──┘ └───┘
pid ┴ └───┘
st ──────────────┘└─
390 end⟩
st ──┘
391
392 end tychonoff
393
394 instance quot.compact_space {r : α → α → Prop} [compact_space α] :
id ┴ ┴ └───────────┘ ┴
src └───────────┘
typ ┴ ┴ └───────────┘ ┴
doc └───────────┘
395 compact_space (quot r) :=
id └───────────┘ └──┘ ┴
src └───────────┘
typ └───────────┘ └──┘ ┴
doc └───────────┘
396 ⟨by { rw ← range_quot_mk, exact compact_range continuous_quot_mk }⟩
id └───────────┘ └───────────┘ └────────────────┘
src └───┘└───────────┘ └────┘└───────────┘┴└────────────────┘┴
typ └───┘└───────────┘ └────┘└───────────┘┴└────────────────┘┴
doc └───┘ └────┘ ┴ ┴
txt └───┘ └────┘ ┴ ┴
par └───┘ └────┘ ┴ ┴
pid └─┘ ┴ ┴ ┴
st └───────────────────┘└───────────────────────────────────────┘└┘
397
398 instance quotient.compact_space {s : setoid α} [compact_space α] :
id └────┘ ┴ └───────────┘ ┴
src └────┘ └───────────┘
typ └────┘ ┴ └───────────┘ ┴
doc └───────────┘
399 compact_space (quotient s) :=
id └───────────┘ └──────┘ ┴
src └───────────┘ └──────┘
typ └───────────┘ └──────┘ ┴
doc └───────────┘
400 quot.compact_space
id └────────────────┘
src └────────────────┘
typ └────────────────┘
401
402 /-- There are various definitions of "locally compact space" in the literature, which agree for
403 Hausdorff spaces but not in general. This one is the precise condition on X needed for the
404 evaluation `map C(X, Y) × X → Y` to be continuous for all `Y` when `C(X, Y)` is given the
405 compact-open topology. -/
406 class locally_compact_space (α : Type*) [topological_space α] : Prop :=
id └───┘ └───────────────┘ ┴
src └───────────────┘
typ └───┘ └───────────────┘ ┴
doc └───────────────┘
407 (local_compact_nhds : ∀ (x : α) (n ∈ 𝓝 x), ∃ s ∈ 𝓝 x, s ⊆ n ∧ compact s)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └─────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ └─────┘ ┴
doc ┴ ┴ └─────┘
408
409 end compact
410
411 section clopen
412
413 /-- A set is clopen if it is both open and closed. -/
414 def is_clopen (s : set α) : Prop :=
id └─┘ ┴
src └─┘
typ └─┘ ┴
415 is_open s ∧ is_closed s
id └─────┘ ┴ ┴ └───────┘ ┴
src └─────┘ ┴ └───────┘
typ └─────┘ ┴ ┴ └───────┘ ┴
doc └─────┘ └───────┘
416
417 theorem is_clopen_union {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s ∪ t) :=
id └─┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴ ┴ ┴
src └─┘ └───────┘ └───────┘ └───────┘ ┴
typ └─┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴ ┴ ┴
doc └───────┘ └───────┘ └───────┘
418 ⟨is_open_union hs.1 ht.1, is_closed_union hs.2 ht.2⟩
id └───────────┘ └┘┴ └┘┴ └─────────────┘ └┘┴ └┘┴
src └───────────┘ ┴ ┴ └─────────────┘ ┴ ┴
typ └───────────┘ └┘┴ └┘┴ └─────────────┘ └┘┴ └┘┴
419
420 theorem is_clopen_inter {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s ∩ t) :=
id └─┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴ ┴ ┴
src └─┘ └───────┘ └───────┘ └───────┘ ┴
typ └─┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴ ┴ ┴
doc └───────┘ └───────┘ └───────┘
421 ⟨is_open_inter hs.1 ht.1, is_closed_inter hs.2 ht.2⟩
id └───────────┘ └┘┴ └┘┴ └─────────────┘ └┘┴ └┘┴
src └───────────┘ ┴ ┴ └─────────────┘ ┴ ┴
typ └───────────┘ └┘┴ └┘┴ └─────────────┘ └┘┴ └┘┴
422
423 @[simp] theorem is_clopen_empty : is_clopen (∅ : set α) :=
id └───────┘ ┴ └─┘ ┴
src └───────┘ ┴ └─┘
typ └───────┘ ┴ └─┘ ┴
doc └──┘ └───────┘
424 ⟨is_open_empty, is_closed_empty⟩
id └───────────┘ └─────────────┘
src └───────────┘ └─────────────┘
typ └───────────┘ └─────────────┘
425
426 @[simp] theorem is_clopen_univ : is_clopen (univ : set α) :=
id └───────┘ └──┘ └─┘ ┴
src └───────┘ └──┘ └─┘
typ └───────┘ └──┘ └─┘ ┴
doc └──┘ └───────┘
427 ⟨is_open_univ, is_closed_univ⟩
id └──────────┘ └────────────┘
src └──────────┘ └────────────┘
typ └──────────┘ └────────────┘
428
429 theorem is_clopen_compl {s : set α} (hs : is_clopen s) : is_clopen (-s) :=
id └─┘ ┴ └───────┘ ┴ └───────┘ ┴┴
src └─┘ └───────┘ └───────┘ ┴
typ └─┘ ┴ └───────┘ ┴ └───────┘ ┴┴
doc └───────┘ └───────┘
430 ⟨hs.2, is_closed_compl_iff.2 hs.1⟩
id └┘┴ └─────────────────┘┴ └┘┴
src ┴ └─────────────────┘┴ ┴
typ └┘┴ └─────────────────┘┴ └┘┴
431
432 @[simp] theorem is_clopen_compl_iff {s : set α} : is_clopen (-s) ↔ is_clopen s :=
id └─┘ ┴ └───────┘ ┴┴ ┴ └───────┘ ┴
src └─┘ └───────┘ ┴ ┴ └───────┘
typ └─┘ ┴ └───────┘ ┴┴ ┴ └───────┘ ┴
doc └──┘ └───────┘ └───────┘
433 ⟨λ h, compl_compl s ▸ is_clopen_compl h, is_clopen_compl⟩
id ┴ └─────────┘ ┴ ┴ └─────────────┘ ┴ └─────────────┘
src └─────────┘ ┴ └─────────────┘ └─────────────┘
typ ┴ └─────────┘ ┴ ┴ └─────────────┘ ┴ └─────────────┘
434
435 theorem is_clopen_diff {s t : set α} (hs : is_clopen s) (ht : is_clopen t) : is_clopen (s-t) :=
id └─┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴┴┴
src └─┘ └───────┘ └───────┘ └───────┘ ┴
typ └─┘ ┴ └───────┘ ┴ └───────┘ ┴ └───────┘ ┴┴┴
doc └───────┘ └───────┘ └───────┘
436 is_clopen_inter hs (is_clopen_compl ht)
id └─────────────┘ └┘ └─────────────┘ └┘
src └─────────────┘ └─────────────┘
typ └─────────────┘ └┘ └─────────────┘ └┘
437
438 end clopen
439
440 section irreducible
441
442 /-- An irreducible set is one where there is no non-trivial pair of disjoint opens. -/
443 def is_irreducible (s : set α) : Prop :=
id └─┘ ┴
src └─┘
typ └─┘ ┴
444 ∀ (u v : set α), is_open u → is_open v →
id └─┘ ┴ └─────┘ ┴ └─────┘ ┴
src └─┘ └─────┘ └─────┘
typ └─┘ ┴ └─────┘ ┴ └─────┘ ┴
doc └─────┘ └─────┘
445 (∃ x, x ∈ s ∩ u) → (∃ x, x ∈ s ∩ v) → ∃ x, x ∈ s ∩ (u ∩ v)
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
446
447 theorem is_irreducible_empty : is_irreducible (∅ : set α) :=
id └────────────┘ ┴ └─┘ ┴
src └────────────┘ ┴ └─┘
typ └────────────┘ ┴ └─┘ ┴
doc └────────────┘
448 λ _ _ _ _ _ ⟨x, h1, h2⟩, h1.elim
id ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───┘
src └───┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └───┘
449
450 theorem is_irreducible_singleton {x} : is_irreducible ({x} : set α) :=
id └────────────┘ ┴┴ └─┘ ┴
src └────────────┘ ┴ └─┘
typ └────────────┘ ┴┴ └─┘ ┴
doc └────────────┘
451 λ u v _ _ ⟨y, h1, h2⟩ ⟨z, h3, h4⟩, by rw mem_singleton_iff at h1 h3;
id ┴ ┴ ┴ ┴ ┴ ┴ └───────────────┘
src └─┘└───────────────┘└───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└───────────────┘└───────┘
doc └─┘ └───────┘
txt └─┘ └───────┘
par └─┘ └───────┘
pid ┴ └───────┘
st └───────────────────────────────
452 substs y z; exact ⟨x, or.inl rfl, h2, h4⟩
id ┴ └────┘ └─┘ └┘ └┘
src └────────┘ └────┘ └┘└────┘┴└─┘└┘ └┘ └─
typ └────────┘ └────┘ ┴└┘└────┘┴└─┘└┘└┘└┘└┘└─
doc └────────┘ └────┘ └┘ ┴ └┘ └┘ └─
txt └────────┘ └────┘ └┘ ┴ └┘ └┘ └─
par └────────┘ └────┘ └┘ ┴ └┘ └┘ └─
pid └──┘ ┴ └┘ ┴ └┘ └┘ ┴└
st ──────────────────────────────────────────
453
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
454 theorem is_irreducible_closure {s : set α} (H : is_irreducible s) :
id └─┘ ┴ └────────────┘ ┴
src └─┘ └────────────┘
typ └─┘ ┴ └────────────┘ ┴
doc └────────────┘
455 is_irreducible (closure s) :=
id └────────────┘ └─────┘ ┴
src └────────────┘ └─────┘
typ └────────────┘ └─────┘ ┴
doc └────────────┘ └─────┘
456 λ u v hu hv ⟨y, hycs, hyu⟩ ⟨z, hzcs, hzv⟩,
id ┴ ┴ └┘ └┘ ┴ └──┘ └─┘ ┴ └──┘ └─┘
typ ┴ ┴ └┘ └┘ ┴ └──┘ └─┘ ┴ └──┘ └─┘
457 let ⟨p, hpu, hps⟩ := mem_closure_iff.1 hycs u hu hyu in
id └─┘ ┴ └─┘ └─┘ └─────────────┘┴ ┴ └┘
src └─────────────┘┴
typ └─┘ ┴ └─┘ └─┘ └─────────────┘┴ ┴ └┘
458 let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 hzcs v hv hzv in
id └─┘ ┴ └─┘ └─┘ └─────────────┘┴ ┴ └┘
src └─────────────┘┴
typ └─┘ ┴ └─┘ └─┘ └─────────────┘┴ ┴ └┘
459 let ⟨r, hrs, hruv⟩ := H u v hu hv ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in
id └─┘ ┴ └─┘ └──┘ ┴ ┴ ┴ └┘ └┘
typ └─┘ ┴ └─┘ └──┘ ┴ ┴ ┴ └┘ └┘
460 ⟨r, subset_closure hrs, hruv⟩
id └────────────┘
src └────────────┘
typ └────────────┘
461
462 theorem exists_irreducible (s : set α) (H : is_irreducible s) :
id └─┘ ┴ └────────────┘ ┴
src └─┘ └────────────┘
typ └─┘ ┴ └────────────┘ ┴
doc └────────────┘
463 ∃ t : set α, is_irreducible t ∧ s ⊆ t ∧ ∀ u, is_irreducible u → t ⊆ u → u = t :=
id ┴ └─┘ ┴┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
typ ┴ └─┘ ┴┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────┘ └────────────┘
464 let ⟨m, hm, hsm, hmm⟩ := zorn.zorn_subset₀ { t : set α | is_irreducible t }
id └─┘ ┴ └┘ └─┘ └─┘ └───────────────┘ ┴ └─┘ ┴ └────────────┘ ┴
src └───────────────┘ ┴ └─┘ └────────────┘
typ └─┘ ┴ └┘ └─┘ └─┘ └───────────────┘ ┴ └─┘ ┴ └────────────┘ ┴
doc └────────────┘
465 (λ c hc hcc hcn, let ⟨t, htc⟩ := hcn in
id ┴ └┘ └─┘ └─┘ └─┘ └─┘
typ ┴ └┘ └─┘ └─┘ └─┘ └─┘
466 ⟨⋃₀ c, λ u v hu hv ⟨y, hy, hyu⟩ ⟨z, hz, hzv⟩,
id └┘ ┴ ┴ ┴ └┘ └┘ ┴┴ └┘ └─┘ ┴┴ └┘ └─┘
src └┘
typ └┘ ┴ ┴ ┴ └┘ └┘ ┴┴ └┘ └─┘ ┴┴ └┘ └─┘
467 let ⟨p, hpc, hyp⟩ := mem_sUnion.1 hy,
id └─┘ ┴ └─┘ └─┘ └────────┘┴
src └────────┘┴
typ └─┘ ┴ └─┘ └─┘ └────────┘┴
468 ⟨q, hqc, hzq⟩ := mem_sUnion.1 hz in
id ┴ └─┘ └─┘ └────────┘┴
src └────────┘┴
typ ┴ └─┘ └─┘ └────────┘┴
469 or.cases_on (zorn.chain.total hcc hpc hqc)
id └─────────┘ └──────────────┘ └─┘
src └─────────┘ └──────────────┘
typ └─────────┘ └──────────────┘ └─┘
470 (assume hpq : p ⊆ q, let ⟨x, hxp, hxuv⟩ := hc hqc u v hu hv
id ┴ └─┘ ┴ └─┘ └──┘ └┘ ┴ ┴ └┘ └┘
src ┴
typ ┴ └─┘ ┴ └─┘ └──┘ └┘ ┴ ┴ └┘ └┘
471 ⟨y, hpq hyp, hyu⟩ ⟨z, hzq, hzv⟩ in
id └─┘
typ └─┘
472 ⟨x, mem_sUnion_of_mem hxp hqc, hxuv⟩)
id └───────────────┘
src └───────────────┘
typ └───────────────┘
473 (assume hqp : q ⊆ p, let ⟨x, hxp, hxuv⟩ := hc hpc u v hu hv
id ┴ └─┘ ┴ └─┘ └──┘ └┘ ┴ ┴ └┘ └┘
src ┴
typ ┴ └─┘ ┴ └─┘ └──┘ └┘ ┴ ┴ └┘ └┘
474 ⟨y, hyp, hyu⟩ ⟨z, hqp hzq, hzv⟩ in
id └─┘
typ └─┘
475 ⟨x, mem_sUnion_of_mem hxp hpc, hxuv⟩),
id └───────────────┘
src └───────────────┘
typ └───────────────┘
476 λ x hxc, set.subset_sUnion_of_mem hxc⟩) s H in
id ┴ └─┘ └──────────────────────┘ └─┘ ┴ ┴
src └──────────────────────┘
typ ┴ └─┘ └──────────────────────┘ └─┘ ┴ ┴
477 ⟨m, hm, hsm, λ u hu hmu, hmm _ hu hmu⟩
id ┴ └┘ └─┘ └┘ └─┘
typ ┴ └┘ └─┘ └┘ └─┘
478
479 /-- A maximal irreducible set that contains a given point. -/
480 def irreducible_component (x : α) : set α :=
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
481 classical.some (exists_irreducible {x} is_irreducible_singleton)
id └────────────┘ └────────────────┘ ┴┴ └──────────────────────┘
src └────────────┘ └────────────────┘ ┴ └──────────────────────┘
typ └────────────┘ └────────────────┘ ┴┴ └──────────────────────┘
482
483 theorem is_irreducible_irreducible_component {x : α} : is_irreducible (irreducible_component x) :=
id ┴ └────────────┘ └───────────────────┘ ┴
src └────────────┘ └───────────────────┘
typ ┴ └────────────┘ └───────────────────┘ ┴
doc └────────────┘ └───────────────────┘
484 (classical.some_spec (exists_irreducible {x} is_irreducible_singleton)).1
id └─────────────────┘ └────────────────┘ ┴┴ └──────────────────────┘ ┴
src └─────────────────┘ └────────────────┘ ┴ └──────────────────────┘ ┴
typ └─────────────────┘ └────────────────┘ ┴┴ └──────────────────────┘ ┴
485
486 theorem mem_irreducible_component {x : α} : x ∈ irreducible_component x :=
id ┴ ┴ ┴ └───────────────────┘ ┴
src ┴ └───────────────────┘
typ ┴ ┴ ┴ └───────────────────┘ ┴
doc └───────────────────┘
487 singleton_subset_iff.1
id └──────────────────┘┴
src └──────────────────┘┴
typ └──────────────────┘┴
488 (classical.some_spec (exists_irreducible {x} is_irreducible_singleton)).2.1
id └─────────────────┘ └────────────────┘ ┴┴ └──────────────────────┘ ┴ ┴
src └─────────────────┘ └────────────────┘ ┴ └──────────────────────┘ ┴ ┴
typ └─────────────────┘ └────────────────┘ ┴┴ └──────────────────────┘ ┴ ┴
489
490 theorem eq_irreducible_component {x : α} :
id ┴
typ ┴
491 ∀ {s : set α}, is_irreducible s → irreducible_component x ⊆ s → s = irreducible_component x :=
id └─┘ ┴ └────────────┘ ┴ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴
src └─┘ └────────────┘ └───────────────────┘ ┴ ┴ └───────────────────┘
typ └─┘ ┴ └────────────┘ ┴ └───────────────────┘ ┴ ┴ ┴ ┴ ┴ └───────────────────┘ ┴
doc └────────────┘ └───────────────────┘ └───────────────────┘
492 (classical.some_spec (exists_irreducible {x} is_irreducible_singleton)).2.2
id └─────────────────┘ └────────────────┘ ┴┴ └──────────────────────┘ ┴ ┴
src └─────────────────┘ └────────────────┘ ┴ └──────────────────────┘ ┴ ┴
typ └─────────────────┘ └────────────────┘ ┴┴ └──────────────────────┘ ┴ ┴
493
494 theorem is_closed_irreducible_component {x : α} :
id ┴
typ ┴
495 is_closed (irreducible_component x) :=
id └───────┘ └───────────────────┘ ┴
src └───────┘ └───────────────────┘
typ └───────┘ └───────────────────┘ ┴
doc └───────┘ └───────────────────┘
496 closure_eq_iff_is_closed.1 $ eq_irreducible_component
id └──────────────────────┘┴ └──────────────────────┘
src └──────────────────────┘┴ └──────────────────────┘
typ └──────────────────────┘┴ └──────────────────────┘
497 (is_irreducible_closure is_irreducible_irreducible_component)
id └────────────────────┘ └──────────────────────────────────┘
src └────────────────────┘ └──────────────────────────────────┘
typ └────────────────────┘ └──────────────────────────────────┘
498 subset_closure
id └────────────┘
src └────────────┘
typ └────────────┘
499
500 /-- An irreducible space is one where there is no non-trivial pair of disjoint opens. -/
501 class irreducible_space (α : Type u) [topological_space α] : Prop :=
id └──┘ └───────────────┘ ┴
src └───────────────┘
typ └──┘ └───────────────┘ ┴
doc └───────────────┘
502 (is_irreducible_univ : is_irreducible (univ : set α))
id └────────────┘ └──┘ └─┘ ┴
src └────────────┘ └──┘ └─┘
typ └────────────┘ └──┘ └─┘ ┴
doc └────────────┘
503
504 theorem irreducible_exists_mem_inter [irreducible_space α] {s t : set α} :
id └───────────────┘ ┴ └─┘ ┴
src └───────────────┘ └─┘
typ └───────────────┘ ┴ └─┘ ┴
doc └───────────────┘
505 is_open s → is_open t → (∃ x, x ∈ s) → (∃ x, x ∈ t) → ∃ x, x ∈ s ∩ t :=
id └─────┘ ┴ └─────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └─────┘ ┴ └─────┘ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
506 by simpa only [univ_inter, univ_subset_iff] using
id └────────┘ └─────────────┘
src └──────────┘└────────┘└┘└─────────────┘└───────
typ └──────────┘└────────┘└┘└─────────────┘└───────
doc └──────────┘ └┘ └───────
txt └──────────┘ └┘ └───────
par └──────────┘ └┘ └───────
pid ┴└──┘└┘ └┘ ┴┴└─────
st └───────────────────────────────────────────────
507 @irreducible_space.is_irreducible_univ α _ _ s t
id └───────────────────────────────────┘ ┴ ┴ ┴
src ─┘ └───────────────────────────────────┘┴ └───┘ ┴ └
typ ─┘ └───────────────────────────────────┘┴┴└───┘┴┴┴└
doc ─┘ ┴ └───┘ ┴ └
txt ─┘ ┴ └───┘ ┴ └
par ─┘ ┴ └───┘ ┴ └
pid ─┘ ┴ └───┘ ┴ └
st ───────────────────────────────────────────────────
508
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
509 end irreducible
510
511 section connected
512
513 /-- A connected set is one where there is no non-trivial open partition. -/
514 def is_connected (s : set α) : Prop :=
id └─┘ ┴
src └─┘
typ └─┘ ┴
515 ∀ (u v : set α), is_open u → is_open v → s ⊆ u ∪ v →
id └─┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─────┘ └─────┘ ┴ ┴
typ └─┘ ┴ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘
516 (∃ x, x ∈ s ∩ u) → (∃ x, x ∈ s ∩ v) → ∃ x, x ∈ s ∩ (u ∩ v)
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
517
518 theorem is_connected_of_is_irreducible {s : set α} (H : is_irreducible s) : is_connected s :=
id └─┘ ┴ └────────────┘ ┴ └──────────┘ ┴
src └─┘ └────────────┘ └──────────┘
typ └─┘ ┴ └────────────┘ ┴ └──────────┘ ┴
doc └────────────┘ └──────────┘
519 λ _ _ hu hv _, H _ _ hu hv
id ┴ ┴ └┘ └┘ ┴ ┴ └┘ └┘
typ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └┘
520
521 theorem is_connected_empty : is_connected (∅ : set α) :=
id └──────────┘ ┴ └─┘ ┴
src └──────────┘ ┴ └─┘
typ └──────────┘ ┴ └─┘ ┴
doc └──────────┘
522 is_connected_of_is_irreducible is_irreducible_empty
id └────────────────────────────┘ └──────────────────┘
src └────────────────────────────┘ └──────────────────┘
typ └────────────────────────────┘ └──────────────────┘
523
524 theorem is_connected_singleton {x} : is_connected ({x} : set α) :=
id └──────────┘ ┴┴ └─┘ ┴
src └──────────┘ ┴ └─┘
typ └──────────┘ ┴┴ └─┘ ┴
doc └──────────┘
525 is_connected_of_is_irreducible is_irreducible_singleton
id └────────────────────────────┘ └──────────────────────┘
src └────────────────────────────┘ └──────────────────────┘
typ └────────────────────────────┘ └──────────────────────┘
526
527 /-- If any point of a set is joined to a fixed point by a connected subset,
528 then the original set is connected as well. -/
529 theorem is_connected_of_forall {s : set α} (x : α)
id └─┘ ┴ ┴
src └─┘
typ └─┘ ┴ ┴
530 (H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ is_connected t) :
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘
531 is_connected s :=
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
532 begin
st └─────
533 rintros u v hu hv hs ⟨z, zs, zu⟩ ⟨y, ys, yv⟩,
src └──────────────────────────────────────────┘
typ └──────────────────────────────────────────┘
doc └──────────────────────────────────────────┘
txt └──────────────────────────────────────────┘
par └──────────────────────────────────────────┘
pid └───────────────────────────────────┘
st ─────────────────────────────────────────────┘└─
534 have xs : x ∈ s, by { rcases H y ys with ⟨t, ts, xt, yt, ht⟩, exact ts xt },
id ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘
src └────────┘ ┴┴┴ └─────┘ ┴ ┴ └───────────────────────┘ └────┘ ┴ ┴
typ └────────┘┴┴┴┴┴ └─────┘┴┴┴┴└┘└───────────────────────┘ └────┘└┘┴└┘┴
doc └────────┘ ┴ ┴ └─────┘ ┴ ┴ └───────────────────────┘ └────┘ ┴ ┴
txt └────────┘ ┴ ┴ └─────┘ ┴ ┴ └───────────────────────┘ └────┘ ┴ ┴
par └────────┘ ┴ ┴ └─────┘ ┴ ┴ └───────────────────────┘ └────┘ ┴ ┴
pid └─────┘└─┘ ┴ ┴ ┴ ┴ ┴ └───────────────────────┘ ┴ ┴ ┴
st ────────────────┘ ┴└─────────────────────────────────────┘└────────────┘└┘└
535 wlog xu : x ∈ u := hs xs using [u v y z, v u z y],
id ┴ ┴ └┘ └┘
src └────────┘ ┴ ┴ └──┘ ┴ └───────────────────────┘
typ └────────┘┴┴ ┴┴└──┘└┘┴└┘└───────────────────────┘
doc └────────┘ ┴ ┴ └──┘ ┴ └───────────────────────┘
txt └────────┘ ┴ ┴ └──┘ ┴ └───────────────────────┘
par └────────┘ ┴ ┴ └──┘ ┴ └───────────────────────┘
pid └─┘└─┘ ┴ ┴ └──┘ ┴ └───────────────────────┘
st ──────────────────────────────────────────────────┘└─
536 { rcases H y ys with ⟨t, ts, xt, yt, ht⟩,
id ┴ ┴ └┘
src └─────┘ ┴ ┴ └───────────────────────┘
typ └─────┘┴┴┴┴└┘└───────────────────────┘
doc └─────┘ ┴ ┴ └───────────────────────┘
txt └─────┘ ┴ ┴ └───────────────────────┘
par └─────┘ ┴ ┴ └───────────────────────┘
pid ┴ ┴ ┴ └───────────────────────┘
st ───┘└────────────────────────────────────┘└─
537 have := ht u v hu hv(subset.trans ts hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩,
id └┘ ┴ ┴ └┘ └┘ └──────────┘ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘
src └──────┘ ┴ ┴ ┴ ┴ └──────────┘┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
typ └──────┘└┘┴┴┴┴┴└┘┴└┘ └──────────┘┴└┘┴└┘└┘ ┴└┘└┘└┘└┘└┘ ┴└┘└┘└┘└┘┴
doc └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
par └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
st ───────────────────────────────────────────────────────────────────┘└─
538 exact this.imp (λ z hz, ⟨ts hz.1, hz.2⟩) },
id └──────┘ └┘
src └────┘└──────┘┴ └─────┘ ┴ └──┘ └───┘
typ └────┘└──────┘┴ └─────┘ └┘┴ └──┘ └───┘
doc └────┘ ┴ └─────┘ ┴ └──┘ └───┘
txt └────┘ ┴ └─────┘ ┴ └──┘ └───┘
par └────┘ ┴ └─────┘ ┴ └──┘ └───┘
pid ┴ ┴ └─────┘ ┴ └──┘ └──┘┴
st ────────────────────────────────────────────┘└┘└
539 { rw [union_comm v, inter_comm v] at this,
id └────────┘ ┴ └────────┘ ┴
src └──┘└────────┘┴ └┘└────────┘┴ └───────┘
typ └──┘└────────┘┴┴└┘└────────┘┴┴└───────┘
doc └──┘ ┴ └┘ ┴ └───────┘
txt └──┘ ┴ └┘ ┴ └───────┘
par └──┘ ┴ └┘ ┴ └───────┘
pid └┘ ┴ └┘ ┴ ┴└──────┘
st ───────────────────┘└────────────┘┴└──────┘└─
540 apply this; assumption }
src └────┘ └─────────┘
typ └────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ ┴
st ──────────────────────────┘└─
541 end
st ──┘
542
543 /-- If any two points of a set are contained in a connected subset,
544 then the original set is connected as well. -/
545 theorem is_connected_of_forall_pair {s : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
546 (H : ∀ x y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ is_connected t) :
id ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘
typ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴
doc └──────────┘
547 is_connected s :=
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
548 begin
st └─────
549 rintros u v hu hv hs ⟨x, xs, xu⟩ ⟨y, ys, yv⟩,
src └──────────────────────────────────────────┘
typ └──────────────────────────────────────────┘
doc └──────────────────────────────────────────┘
txt └──────────────────────────────────────────┘
par └──────────────────────────────────────────┘
pid └───────────────────────────────────┘
st ─────────────────────────────────────────────┘└─
550 rcases H x y xs ys with ⟨t, ts, xt, yt, ht⟩,
id ┴ ┴ ┴ └┘ └┘
src └─────┘ ┴ ┴ ┴ ┴ └───────────────────────┘
typ └─────┘┴┴┴┴┴┴└┘┴└┘└───────────────────────┘
doc └─────┘ ┴ ┴ ┴ ┴ └───────────────────────┘
txt └─────┘ ┴ ┴ ┴ ┴ └───────────────────────┘
par └─────┘ ┴ ┴ ┴ ┴ └───────────────────────┘
pid ┴ ┴ ┴ ┴ ┴ └───────────────────────┘
st ────────────────────────────────────────────┘└─
551 have := ht u v hu hv(subset.trans ts hs) ⟨x, xt, xu⟩ ⟨y, yt, yv⟩,
id └┘ ┴ ┴ └┘ └┘ └──────────┘ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘
src └──────┘ ┴ ┴ ┴ ┴ └──────────┘┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
typ └──────┘└┘┴┴┴┴┴└┘┴└┘ └──────────┘┴└┘┴└┘└┘ ┴└┘└┘└┘└┘└┘ ┴└┘└┘└┘└┘┴
doc └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
txt └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
par └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
pid └───┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └┘ └┘ └┘ └┘ └┘ ┴
st ─────────────────────────────────────────────────────────────────┘└─
552 exact this.imp (λ z hz, ⟨ts hz.1, hz.2⟩)
id └──────┘ └┘
src └────┘└──────┘┴ └─────┘ ┴ └──┘ └───┘
typ └────┘└──────┘┴ └─────┘ └┘┴ └──┘ └───┘
doc └────┘ ┴ └─────┘ ┴ └──┘ └───┘
txt └────┘ ┴ └─────┘ ┴ └──┘ └───┘
par └────┘ ┴ └─────┘ ┴ └──┘ └───┘
pid ┴ ┴ └─────┘ ┴ └──┘ └──┘┴
st ──────────────────────────────────────────┘
553 end
st └─┘
554
555 /-- A union of a family of connected sets with a common point is connected as well. -/
556 theorem is_connected_sUnion (x : α) (c : set (set α)) (H1 : ∀ s ∈ c, x ∈ s)
id ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └─┘ ┴
typ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ ┴ ┴
557 (H2 : ∀ s ∈ c, is_connected s) : is_connected (⋃₀ c) :=
id ┴ ┴ └──────────┘ ┴ └──────────┘ └┘ ┴
src └──────────┘ └──────────┘ └┘
typ ┴ ┴ └──────────┘ ┴ └──────────┘ └┘ ┴
doc └──────────┘ └──────────┘
558 begin
st └─────
559 apply is_connected_of_forall x,
id └────────────────────┘ ┴
src └────┘└────────────────────┘┴
typ └────┘└────────────────────┘┴┴
doc └────┘└────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────┘└─
560 rintros y ⟨s, sc, ys⟩,
src └───────────────────┘
typ └───────────────────┘
doc └───────────────────┘
txt └───────────────────┘
par └───────────────────┘
pid └────────────┘
st ──────────────────────┘└─
561 exact ⟨s, subset_sUnion_of_mem sc, H1 s sc, ys, H2 s sc⟩
id └──────────────────┘ └┘ └┘ └┘ ┴ └┘
src └────┘ └┘└──────────────────┘┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘
typ └────┘ └┘└──────────────────┘┴ └┘└┘┴ ┴ └┘└┘└┘└┘┴┴┴└┘└┘
doc └────┘ └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘
txt └────┘ └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘
par └────┘ └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └┘
pid ┴ └┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────┘
562 end
st └─┘
563
564 theorem is_connected.union (x : α) {s t : set α} (H1 : x ∈ s) (H2 : x ∈ t)
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
565 (H3 : is_connected s) (H4 : is_connected t) : is_connected (s ∪ t) :=
id └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
src └──────────┘ └──────────┘ └──────────┘ ┴
typ └──────────┘ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘ └──────────┘
566 sUnion_pair s t ▸ is_connected_sUnion x {s, t}
id └─────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴┴┴ ┴
src └─────────┘ ┴ └─────────────────┘ ┴ ┴
typ └─────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴┴┴ ┴
doc └─────────────────┘
567 (by rintro r (rfl | rfl | h); [exact H2, exact H1, exact h.elim])
id ┴ └┘ └┘ └────┘
src └──────────────────────┘ ┴└────┘ └────┘ └────┘└────┘
typ └──────────────────────┘ ┴└────┘└┘ └────┘└┘ └────┘└────┘
doc └──────────────────────┘ └────┘ └────┘ └────┘
txt └──────────────────────┘ └────┘ └────┘ └────┘
par └──────────────────────┘ └────┘ └────┘ └────┘
pid └────────────────┘ ┴ ┴ ┴
st └───────────────────────────────────────────────────────────┘
568 (by rintro r (rfl | rfl | h); [exact H4, exact H3, exact h.elim])
id ┴ └┘ └┘ └────┘
src └──────────────────────┘ ┴└────┘ └────┘ └────┘└────┘
typ └──────────────────────┘ ┴└────┘└┘ └────┘└┘ └────┘└────┘
doc └──────────────────────┘ └────┘ └────┘ └────┘
txt └──────────────────────┘ └────┘ └────┘ └────┘
par └──────────────────────┘ └────┘ └────┘ └────┘
pid └────────────────┘ ┴ ┴ ┴
st └───────────────────────────────────────────────────────────┘
569
570 theorem is_connected.closure {s : set α} (H : is_connected s) :
id └─┘ ┴ └──────────┘ ┴
src └─┘ └──────────┘
typ └─┘ ┴ └──────────┘ ┴
doc └──────────┘
571 is_connected (closure s) :=
id └──────────┘ └─────┘ ┴
src └──────────┘ └─────┘
typ └──────────┘ └─────┘ ┴
doc └──────────┘ └─────┘
572 λ u v hu hv hcsuv ⟨y, hycs, hyu⟩ ⟨z, hzcs, hzv⟩,
id ┴ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ ┴ └──┘ └─┘
typ ┴ ┴ └┘ └┘ └───┘ ┴ └──┘ └─┘ ┴ └──┘ └─┘
573 let ⟨p, hpu, hps⟩ := mem_closure_iff.1 hycs u hu hyu in
id └─┘ ┴ └─┘ └─┘ └─────────────┘┴ ┴ └┘
src └─────────────┘┴
typ └─┘ ┴ └─┘ └─┘ └─────────────┘┴ ┴ └┘
574 let ⟨q, hqv, hqs⟩ := mem_closure_iff.1 hzcs v hv hzv in
id └─┘ ┴ └─┘ └─┘ └─────────────┘┴ ┴ └┘
src └─────────────┘┴
typ └─┘ ┴ └─┘ └─┘ └─────────────┘┴ ┴ └┘
575 let ⟨r, hrs, hruv⟩ := H u v hu hv (subset.trans subset_closure hcsuv) ⟨p, hps, hpu⟩ ⟨q, hqs, hqv⟩ in
id └─┘ ┴ └─┘ └──┘ ┴ ┴ ┴ └┘ └┘ └──────────┘ └────────────┘ └───┘
src └──────────┘ └────────────┘
typ └─┘ ┴ └─┘ └──┘ ┴ ┴ ┴ └┘ └┘ └──────────┘ └────────────┘ └───┘
576 ⟨r, subset_closure hrs, hruv⟩
id └────────────┘
src └────────────┘
typ └────────────┘
577
578 theorem is_connected.image [topological_space β] {s : set α} (H : is_connected s)
id └───────────────┘ ┴ └─┘ ┴ └──────────┘ ┴
src └───────────────┘ └─┘ └──────────┘
typ └───────────────┘ ┴ └─┘ ┴ └──────────┘ ┴
doc └───────────────┘ └──────────┘
579 (f : α → β) (hf : continuous_on f s) : is_connected (f '' s) :=
id ┴ ┴ └───────────┘ ┴ ┴ └──────────┘ ┴ └┘ ┴
src └───────────┘ └──────────┘ └┘
typ ┴ ┴ └───────────┘ ┴ ┴ └──────────┘ ┴ └┘ ┴
doc └───────────┘ └──────────┘
580 begin
st └─────
581 -- Unfold/destruct definitions in hypotheses
st ───────────────────────────────────────────────
582 rintros u v hu hv huv ⟨_, ⟨x, xs, rfl⟩, xu⟩ ⟨_, ⟨y, ys, rfl⟩, yv⟩,
src └───────────────────────────────────────────────────────────────┘
typ └───────────────────────────────────────────────────────────────┘
doc └───────────────────────────────────────────────────────────────┘
txt └───────────────────────────────────────────────────────────────┘
par └───────────────────────────────────────────────────────────────┘
pid └────────────────────────────────────────────────────────┘
st ──────────────────────────────────────────────────────────────────┘└─
583 rcases continuous_on_iff'.1 hf u hu with ⟨u', hu', u'_eq⟩,
id └────────────────┘ └┘ ┴ └┘
src └─────┘└────────────────┘└─┘ ┴ ┴ └────────────────────┘
typ └─────┘└────────────────┘└─┘└┘┴┴┴└┘└────────────────────┘
doc └─────┘ └─┘ ┴ ┴ └────────────────────┘
txt └─────┘ └─┘ ┴ ┴ └────────────────────┘
par └─────┘ └─┘ ┴ ┴ └────────────────────┘
pid ┴ └─┘ ┴ ┴ └────────────────────┘
st ──────────────────────────────────────────────────────────┘└─
584 rcases continuous_on_iff'.1 hf v hv with ⟨v', hv', v'_eq⟩,
id └────────────────┘ └┘ ┴ └┘
src └─────┘└────────────────┘└─┘ ┴ ┴ └────────────────────┘
typ └─────┘└────────────────┘└─┘└┘┴┴┴└┘└────────────────────┘
doc └─────┘ └─┘ ┴ ┴ └────────────────────┘
txt └─────┘ └─┘ ┴ ┴ └────────────────────┘
par └─────┘ └─┘ ┴ ┴ └────────────────────┘
pid ┴ └─┘ ┴ ┴ └────────────────────┘
st ──────────────────────────────────────────────────────────┘└─
585 -- Reformulate `huv : f '' s ⊆ u ∪ v` in terms of `u'` and `v'`
st ──────────────────────────────────────────────────────────────────
586 replace huv : s ⊆ u' ∪ v',
id ┴ ┴ └┘ ┴ └┘
src └────────────┘ ┴┴┴ ┴┴┴
typ └────────────┘┴┴┴┴└┘┴┴┴└┘
doc └────────────┘ ┴ ┴ ┴ ┴
txt └────────────┘ ┴ ┴ ┴ ┴
par └────────────┘ ┴ ┴ ┴ ┴
pid └──┘└─┘ ┴ ┴ ┴ ┴
st ──────────────────────────┘└─
587 { rw [image_subset_iff, preimage_union] at huv,
id └──────────────┘ └────────────┘
src └──┘└──────────────┘└┘└────────────┘└──────┘
typ └──┘└──────────────┘└┘└────────────┘└──────┘
doc └──┘└──────────────┘└┘ └──────┘
txt └──┘ └┘ └──────┘
par └──┘ └┘ └──────┘
pid └┘ └┘ ┴└─────┘
st ───┘└──────────────────┘└──────────────┘┴└─────┘└─
588 replace huv := subset_inter huv (subset.refl _),
id └──────────┘ └─┘ └─────────┘
src └─────────────┘└──────────┘┴ ┴ └─────────┘└─┘
typ └─────────────┘└──────────┘┴└─┘┴ └─────────┘└─┘
doc └─────────────┘ ┴ ┴ └─┘
txt └─────────────┘ ┴ ┴ └─┘
par └─────────────┘ ┴ ┴ └─┘
pid └──┘┴└─┘ ┴ ┴ └─┘
st ──────────────────────────────────────────────────┘└─
589 rw [inter_distrib_right, u'_eq, v'_eq, ← inter_distrib_right] at huv,
id └─────────────────┘ └───┘ └───┘ └─────────────────┘
src └──┘└─────────────────┘└┘ └┘ └──┘└─────────────────┘└──────┘
typ └──┘└─────────────────┘└┘└───┘└┘└───┘└──┘└─────────────────┘└──────┘
doc └──┘ └┘ └┘ └──┘ └──────┘
txt └──┘ └┘ └┘ └──┘ └──────┘
par └──┘ └┘ └┘ └──┘ └──────┘
pid └┘ └┘ └┘ └──┘ ┴└─────┘
st ──────────────────────────┘└─────┘└─────┘└─────────────────────┘┴└─────┘└─
590 exact (subset_inter_iff.1 huv).1 },
id └──────────────┘ └─┘
src └────┘ └──────────────┘└─┘ └──┘
typ └────┘ └──────────────┘└─┘└─┘└──┘
doc └────┘ └─┘ └──┘
txt └────┘ └─┘ └──┘
par └────┘ └─┘ └──┘
pid ┴ └─┘ ┴└─┘
st ────────────────────────────────────┘└┘└
591 -- Now `s ⊆ u' ∪ v'`, so we can apply `‹is_connected s›`
st ───────────────────────────────────────────────────────────
592 obtain ⟨z, hz⟩ : (s ∩ (u' ∩ v')).nonempty,
id ┴ ┴ └┘ └┘
src └───────────────┘ ┴┴┴ ┴ ┴ └─────────┘
typ └───────────────┘ ┴┴┴┴ └┘┴ ┴└┘└─────────┘
doc └───────────────┘ ┴ ┴ ┴ ┴ └─────────┘
txt └───────────────┘ ┴ ┴ ┴ ┴ └─────────┘
par └───────────────┘ ┴ ┴ ┴ ┴ └─────────┘
pid └─────────┘ ┴ ┴ ┴ ┴ └────────┘┴
st ──────────────────────────────────────────┘└─
593 { refine H u' v' hu' hv' huv ⟨x, _⟩ ⟨y, _⟩; rw inter_comm,
id ┴ └┘ └┘ └─┘ └─┘ └─┘ ┴ ┴ └────────┘
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──┘ └─┘└────────┘
typ └─────┘┴┴└┘┴└┘┴└─┘┴└─┘┴└─┘┴ ┴└───┘ ┴└──┘ └─┘└────────┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──┘ └─┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──┘ └─┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──┘ └─┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └──┘ ┴
st ───┘└───────────────────────────────────────────┘└────────┘└─
594 exacts [u'_eq ▸ ⟨xu, xs⟩, v'_eq ▸ ⟨yv, ys⟩] },
id └───┘ ┴ └┘ └┘ └───┘ └┘ └┘
src └──────┘ ┴┴┴ └┘ └─┘ ┴ ┴ └┘ └─┘
typ └──────┘└───┘┴┴┴ └┘└┘└┘└─┘└───┘┴ ┴ └┘└┘└┘└─┘
doc └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘ └─┘
txt └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘ └─┘
par └──────┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘ └─┘
pid └┘ ┴ ┴ └┘ └─┘ ┴ ┴ └┘ └┘┴
st ───────────────────────────────────────────────┘└┘└
595 rw [← inter_self s, inter_assoc, inter_left_comm s u', ← inter_assoc,
id └────────┘ ┴ └─────────┘ └─────────────┘ ┴ └┘ └─────────┘
src └────┘└────────┘┴ └┘└─────────┘└┘└─────────────┘┴ ┴ └──┘└─────────┘└─
typ └────┘└────────┘┴┴└┘└─────────┘└┘└─────────────┘┴┴┴└┘└──┘└─────────┘└─
doc └────┘ ┴ └┘ └┘ ┴ ┴ └──┘ └─
txt └────┘ ┴ └┘ └┘ ┴ ┴ └──┘ └─
par └────┘ ┴ └┘ └┘ ┴ ┴ └──┘ └─
pid └──┘ ┴ └┘ └┘ ┴ ┴ └──┘ └─
st ───────────────────┘└───────────┘└────────────────────┘└─────────────┘└─
596 inter_comm s, inter_comm s, ← u'_eq, ← v'_eq] at hz,
id └────────┘ ┴ └────────┘ ┴ └───┘ └───┘
src ───┘└────────┘┴ └┘└────────┘┴ └──┘ └──┘ └─────┘
typ ───┘└────────┘┴┴└┘└────────┘┴┴└──┘└───┘└──┘└───┘└─────┘
doc ───┘ ┴ └┘ ┴ └──┘ └──┘ └─────┘
txt ───┘ ┴ └┘ ┴ └──┘ └──┘ └─────┘
par ───┘ ┴ └┘ ┴ └──┘ └──┘ └─────┘
pid ───┘ ┴ └┘ ┴ └──┘ └──┘ ┴└────┘
st ───────────────┘└────────────┘└───────┘└───────┘┴└────┘└─
597 exact ⟨f z, ⟨z, hz.1.2, rfl⟩, hz.1.1, hz.2.1⟩
id ┴ ┴ └─┘ └┘
src └────┘ ┴ └┘ └┘ └────┘└─┘└─┘ └────┘ └────┘
typ └────┘ ┴┴ └┘ ┴└┘ └────┘└─┘└─┘ └────┘└┘└────┘
doc └────┘ ┴ └┘ └┘ └────┘ └─┘ └────┘ └────┘
txt └────┘ ┴ └┘ └┘ └────┘ └─┘ └────┘ └────┘
par └────┘ ┴ └┘ └┘ └────┘ └─┘ └────┘ └────┘
pid ┴ ┴ └┘ └┘ └────┘ └─┘ └────┘ └───┘┴
st ───────────────────────────────────────────────┘
598 end
st └─┘
599
600 theorem is_connected_closed_iff {s : set α} :
id └─┘ ┴
src └─┘
typ └─┘ ┴
601 is_connected s ↔ ∀ t t', is_closed t → is_closed t' → s ⊆ t ∪ t' →
id └──────────┘ ┴ ┴ ┴ └┘ └───────┘ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └┘
src └──────────┘ ┴ └───────┘ └───────┘ ┴ ┴
typ └──────────┘ ┴ ┴ ┴ └┘ └───────┘ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ └┘
doc └──────────┘ └───────┘ └───────┘
602 (s ∩ t).nonempty → (s ∩ t').nonempty → (s ∩ (t ∩ t')).nonempty :=
id ┴ ┴ ┴ └──────┘ ┴ ┴ └┘ └──────┘ ┴ ┴ ┴ ┴ └┘ └──────┘
src ┴ └──────┘ ┴ └──────┘ ┴ ┴ └──────┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴ └┘ └──────┘ ┴ ┴ ┴ ┴ └┘ └──────┘
doc └──────┘ └──────┘ └──────┘
603 ⟨begin
st └─────
604 rintros h t t' ht ht' htt' ⟨x, xs, xt⟩ ⟨y, ys, yt'⟩,
src └─────────────────────────────────────────────────┘
typ └─────────────────────────────────────────────────┘
doc └─────────────────────────────────────────────────┘
txt └─────────────────────────────────────────────────┘
par └─────────────────────────────────────────────────┘
pid └──────────────────────────────────────────┘
st ────────────────────────────────────────────────────┘└─
605 by_contradiction h',
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └─┘
st ────────────────────┘└─
606 rw [← ne_empty_iff_nonempty, ne.def, not_not, ← subset_compl_iff_disjoint, compl_inter] at h',
id └───────────────────┘ └────┘ └─────┘ └───────────────────────┘ └─────────┘
src └────┘└───────────────────┘└┘└────┘└┘└─────┘└──┘└───────────────────────┘└┘└─────────┘└─────┘
typ └────┘└───────────────────┘└┘└────┘└┘└─────┘└──┘└───────────────────────┘└┘└─────────┘└─────┘
doc └────┘ └┘ └┘ └──┘ └┘ └─────┘
txt └────┘ └┘ └┘ └──┘ └┘ └─────┘
par └────┘ └┘ └┘ └──┘ └┘ └─────┘
pid └──┘ └┘ └┘ └──┘ └┘ ┴└────┘
st ────────────────────────────┘└──────┘└───────┘└───────────────────────────┘└───────────┘┴└────┘└─
607 have xt' : x ∉ t', from (h' xs).elim (absurd xt) id,
id ┴ ┴ └┘ └┘ └┘ └────┘ └┘ └┘
src └─────────┘ ┴┴┴ └───┘ ┴ └─────┘ └────┘┴ └┘└┘
typ └─────────┘┴┴┴┴└┘ └───┘ └┘┴└┘└─────┘ └────┘┴└┘└┘└┘
doc └─────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ └┘
txt └─────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ └┘
par └─────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ └┘
pid └──────┘└─┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ └┘
st ──────────────────┘└────────────────────────────────┘└─
608 have yt : y ∉ t, from (h' ys).elim id (absurd yt'),
id ┴ ┴ └┘ └┘ └┘ └────┘ └─┘
src └────────┘ ┴ ┴ └───┘ ┴ └─────┘└┘┴ └────┘┴ ┴
typ └────────┘┴┴ ┴┴ └───┘ └┘┴└┘└─────┘└┘┴ └────┘┴└─┘┴
doc └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴
txt └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴
par └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴
st ────────────────┘└─────────────────────────────────┘└─
609 have := ne_empty_iff_nonempty.2 (h (-t) (-t') (is_open_compl_iff.2 ht)
id └───────────────────┘ ┴ ┴┴ └┘ └┘
src └──────┘└───────────────────┘└─┘ ┴ ┴ └┘ └┘ └─┘ └─
typ └──────┘└───────────────────┘└─┘ ┴┴ ┴┴└┘ └┘└┘ └─┘└┘└─
doc └──────┘ └─┘ ┴ └┘ └┘ └─┘ └─
txt └──────┘ └─┘ ┴ └┘ └┘ └─┘ └─
par └──────┘ └─┘ ┴ └┘ └┘ └─┘ └─
pid └───┘└─┘ └─┘ ┴ └┘ └┘ └─┘ └─
st ─────────────────────────────────────────────────────────────────────────
610 (is_open_compl_iff.2 ht') h' ⟨y, ys, yt⟩ ⟨x, xs, xt'⟩),
id └───────────────┘ └─┘ └┘ ┴ └┘ └┘ ┴ └┘ └─┘
src ───┘ └───────────────┘└─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
typ ───┘ └───────────────┘└─┘└─┘└┘└┘┴ ┴└┘└┘└┘└┘└┘ ┴└┘└┘└┘└─┘└┘
doc ───┘ └─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
txt ───┘ └─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
par ───┘ └─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
pid ───┘ └─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
st ─────────────────────────────────────────────────────────┘└─
611 rw [ne.def, ← compl_union, ← subset_compl_iff_disjoint, compl_compl] at this,
id └────┘ └─────────┘ └───────────────────────┘ └─────────┘
src └──┘└────┘└──┘└─────────┘└──┘└───────────────────────┘└┘└─────────┘└───────┘
typ └──┘└────┘└──┘└─────────┘└──┘└───────────────────────┘└┘└─────────┘└───────┘
doc └──┘ └──┘ └──┘ └┘ └───────┘
txt └──┘ └──┘ └──┘ └┘ └───────┘
par └──┘ └──┘ └──┘ └┘ └───────┘
pid └┘ └──┘ └──┘ └┘ ┴└──────┘
st ───────────┘└─────────────┘└───────────────────────────┘└───────────┘┴└──────┘└─
612 contradiction
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────────────┘
613 end,
st └─┘
614 begin
st └─────
615 rintros h u v hu hv huv ⟨x, xs, xu⟩ ⟨y, ys, yv⟩,
src └─────────────────────────────────────────────┘
typ └─────────────────────────────────────────────┘
doc └─────────────────────────────────────────────┘
txt └─────────────────────────────────────────────┘
par └─────────────────────────────────────────────┘
pid └──────────────────────────────────────┘
st ────────────────────────────────────────────────┘└─
616 by_contradiction h',
src └─────────────────┘
typ └─────────────────┘
doc └─────────────────┘
txt └─────────────────┘
par └─────────────────┘
pid └─┘
st ────────────────────┘└─
617 rw [← set.nonempty, ← ne_empty_iff_nonempty, ne.def, not_not,
id └──────────┘ └───────────────────┘ └────┘ └─────┘
src └────┘└──────────┘└──┘└───────────────────┘└┘└────┘└┘└─────┘└─
typ └────┘└──────────┘└──┘└───────────────────┘└┘└────┘└┘└─────┘└─
doc └────┘└──────────┘└──┘ └┘ └┘ └─
txt └────┘ └──┘ └┘ └┘ └─
par └────┘ └──┘ └┘ └┘ └─
pid └──┘ └──┘ └┘ └┘ └─
st ───────────────────┘└───────────────────────┘└──────┘└───────┘└─
618 ← subset_compl_iff_disjoint, compl_inter] at h',
id └───────────────────────┘ └─────────┘
src ─────┘└───────────────────────┘└┘└─────────┘└─────┘
typ ─────┘└───────────────────────┘└┘└─────────┘└─────┘
doc ─────┘ └┘ └─────┘
txt ─────┘ └┘ └─────┘
par ─────┘ └┘ └─────┘
pid ─────┘ └┘ ┴└────┘
st ──────────────────────────────┘└───────────┘┴└────┘└─
619 have xv : x ∉ v, from (h' xs).elim (absurd xu) id,
id ┴ ┴ └┘ └┘ └────┘ └┘ └┘
src └────────┘ ┴ ┴ └───┘ ┴ └─────┘ └────┘┴ └┘└┘
typ └────────┘┴┴ ┴┴ └───┘ └┘┴└┘└─────┘ └────┘┴└┘└┘└┘
doc └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ └┘
txt └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ └┘
par └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ └┘
pid └─────┘└─┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ └┘
st ────────────────┘└────────────────────────────────┘└─
620 have yu : y ∉ u, from (h' ys).elim id (absurd yv),
id ┴ ┴ └┘ └┘ └┘ └────┘ └┘
src └────────┘ ┴ ┴ └───┘ ┴ └─────┘└┘┴ └────┘┴ ┴
typ └────────┘┴┴ ┴┴ └───┘ └┘┴└┘└─────┘└┘┴ └────┘┴└┘┴
doc └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴
txt └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴
par └────────┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴
pid └─────┘└─┘ ┴ ┴ └───┘ ┴ └─────┘ ┴ ┴ ┴
st ────────────────┘└────────────────────────────────┘└─
621 have := ne_empty_iff_nonempty.2 (h (-u) (-v) (is_closed_compl_iff.2 hu)
id └───────────────────┘ ┴ ┴ ┴ └┘
src └──────┘└───────────────────┘└─┘ ┴ └┘ └┘ └─┘ └─
typ └──────┘└───────────────────┘└─┘ ┴┴ ┴└┘ ┴└┘ └─┘└┘└─
doc └──────┘ └─┘ ┴ └┘ └┘ └─┘ └─
txt └──────┘ └─┘ ┴ └┘ └┘ └─┘ └─
par └──────┘ └─┘ ┴ └┘ └┘ └─┘ └─
pid └───┘└─┘ └─┘ ┴ └┘ └┘ └─┘ └─
st ──────────────────────────────────────────────────────────────────────────
622 (is_closed_compl_iff.2 hv) h' ⟨y, ys, yu⟩ ⟨x, xs, xv⟩),
id └─────────────────┘ └┘ └┘ ┴ └┘ └┘ ┴ └┘ └┘
src ───┘ └─────────────────┘└─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
typ ───┘ └─────────────────┘└─┘└┘└┘└┘┴ ┴└┘└┘└┘└┘└┘ ┴└┘└┘└┘└┘└┘
doc ───┘ └─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
txt ───┘ └─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
par ───┘ └─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
pid ───┘ └─┘ └┘ ┴ └┘ └┘ └┘ └┘ └┘ └┘
st ─────────────────────────────────────────────────────────┘└─
623 rw [ne.def, ← compl_union, ← subset_compl_iff_disjoint, compl_compl] at this,
id └────┘ └─────────┘ └───────────────────────┘ └─────────┘
src └──┘└────┘└──┘└─────────┘└──┘└───────────────────────┘└┘└─────────┘└───────┘
typ └──┘└────┘└──┘└─────────┘└──┘└───────────────────────┘└┘└─────────┘└───────┘
doc └──┘ └──┘ └──┘ └┘ └───────┘
txt └──┘ └──┘ └──┘ └┘ └───────┘
par └──┘ └──┘ └──┘ └┘ └───────┘
pid └┘ └──┘ └──┘ └┘ ┴└──────┘
st ───────────┘└─────────────┘└───────────────────────────┘└───────────┘┴└──────┘└─
624 contradiction
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid ┴
st ───────────────┘
625 end⟩
st └─┘
626
627 /-- The connected component of a point is the maximal connected set
628 that contains this point. -/
629 def connected_component (x : α) : set α :=
id ┴ └─┘ ┴
src └─┘
typ ┴ └─┘ ┴
630 ⋃₀ { s : set α | is_connected s ∧ x ∈ s }
id └┘ ┴ └─┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
src └┘ ┴ └─┘ └──────────┘ ┴ ┴
typ └┘ ┴ └─┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴
doc └──────────┘
631
632 theorem is_connected_connected_component {x : α} : is_connected (connected_component x) :=
id ┴ └──────────┘ └─────────────────┘ ┴
src └──────────┘ └─────────────────┘
typ ┴ └──────────┘ └─────────────────┘ ┴
doc └──────────┘ └─────────────────┘
633 is_connected_sUnion x _ (λ _, and.right) (λ _, and.left)
id └─────────────────┘ ┴ ┴ └───────┘ ┴ └──────┘
src └─────────────────┘ └───────┘ └──────┘
typ └─────────────────┘ ┴ ┴ └───────┘ ┴ └──────┘
doc └─────────────────┘
634
635 theorem mem_connected_component {x : α} : x ∈ connected_component x :=
id ┴ ┴ ┴ └─────────────────┘ ┴
src ┴ └─────────────────┘
typ ┴ ┴ ┴ └─────────────────┘ ┴
doc └─────────────────┘
636 mem_sUnion_of_mem (mem_singleton x) ⟨is_connected_singleton, mem_singleton x⟩
id └───────────────┘ └───────────┘ ┴ └────────────────────┘ └───────────┘ ┴
src └───────────────┘ └───────────┘ └────────────────────┘ └───────────┘
typ └───────────────┘ └───────────┘ ┴ └────────────────────┘ └───────────┘ ┴
637
638 theorem subset_connected_component {x : α} {s : set α} (H1 : is_connected s) (H2 : x ∈ s) :
id ┴ └─┘ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └─┘ └──────────┘ ┴
typ ┴ └─┘ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └──────────┘
639 s ⊆ connected_component x :=
id ┴ ┴ └─────────────────┘ ┴
src ┴ └─────────────────┘
typ ┴ ┴ └─────────────────┘ ┴
doc └─────────────────┘
640 λ z hz, mem_sUnion_of_mem hz ⟨H1, H2⟩
id ┴ └┘ └───────────────┘ └┘ └┘ └┘
src └───────────────┘
typ ┴ └┘ └───────────────┘ └┘ └┘ └┘
641
642 theorem is_closed_connected_component {x : α} :
id ┴
typ ┴
643 is_closed (connected_component x) :=
id └───────┘ └─────────────────┘ ┴
src └───────┘ └─────────────────┘
typ └───────┘ └─────────────────┘ ┴
doc └───────┘ └─────────────────┘
644 closure_eq_iff_is_closed.1 $ subset.antisymm
id └──────────────────────┘┴ └─────────────┘
src └──────────────────────┘┴ └─────────────┘
typ └──────────────────────┘┴ └─────────────┘
645 (subset_connected_component
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
646 is_connected_connected_component.closure
id └──────────────────────────────┘└──────┘
src └──────────────────────────────┘└──────┘
typ └──────────────────────────────┘└──────┘
647 (subset_closure mem_connected_component))
id └────────────┘ └─────────────────────┘
src └────────────┘ └─────────────────────┘
typ └────────────┘ └─────────────────────┘
648 subset_closure
id └────────────┘
src └────────────┘
typ └────────────┘
649
650 theorem irreducible_component_subset_connected_component {x : α} :
id ┴
typ ┴
651 irreducible_component x ⊆ connected_component x :=
id └───────────────────┘ ┴ ┴ └─────────────────┘ ┴
src └───────────────────┘ ┴ └─────────────────┘
typ └───────────────────┘ ┴ ┴ └─────────────────┘ ┴
doc └───────────────────┘ └─────────────────┘
652 subset_connected_component
id └────────────────────────┘
src └────────────────────────┘
typ └────────────────────────┘
653 (is_connected_of_is_irreducible is_irreducible_irreducible_component)
id └────────────────────────────┘ └──────────────────────────────────┘
src └────────────────────────────┘ └──────────────────────────────────┘
typ └────────────────────────────┘ └──────────────────────────────────┘
654 mem_irreducible_component
id └───────────────────────┘
src └───────────────────────┘
typ └───────────────────────┘
655
656 /-- A connected space is one where there is no non-trivial open partition. -/
657 class connected_space (α : Type u) [topological_space α] : Prop :=
id └──┘ └───────────────┘ ┴
src └───────────────┘
typ └──┘ └───────────────┘ ┴
doc └───────────────┘
658 (is_connected_univ : is_connected (univ : set α))
id └──────────┘ └──┘ └─┘ ┴
src └──────────┘ └──┘ └─┘
typ └──────────┘ └──┘ └─┘ ┴
doc └──────────┘
659
660 @[priority 100] -- see Note [lower instance priority]
661 instance irreducible_space.connected_space (α : Type u) [topological_space α]
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
doc └───────────────┘
662 [irreducible_space α] : connected_space α :=
id └───────────────┘ ┴ └─────────────┘ ┴
src └───────────────┘ └─────────────┘
typ └───────────────┘ ┴ └─────────────┘ ┴
doc └───────────────┘ └─────────────┘
663 ⟨is_connected_of_is_irreducible $ irreducible_space.is_irreducible_univ α⟩
id └────────────────────────────┘ └───────────────────────────────────┘ ┴
src └────────────────────────────┘ └───────────────────────────────────┘
typ └────────────────────────────┘ └───────────────────────────────────┘ ┴
664
665 theorem exists_mem_inter [connected_space α] {s t : set α} :
id └─────────────┘ ┴ └─┘ ┴
src └─────────────┘ └─┘
typ └─────────────┘ ┴ └─┘ ┴
doc └─────────────┘
666 is_open s → is_open t → s ∪ t = univ →
id └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └──┘
src └─────┘ └─────┘ ┴ ┴ └──┘
typ └─────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─────┘ └─────┘
667 (∃ x, x ∈ s) → (∃ x, x ∈ t) → ∃ x, x ∈ s ∩ t :=
id ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴ ┴
668 by simpa only [univ_inter, univ_subset_iff] using
id └────────┘ └─────────────┘
src └──────────┘└────────┘└┘└─────────────┘└───────
typ └──────────┘└────────┘└┘└─────────────┘└───────
doc └──────────┘ └┘ └───────
txt └──────────┘ └┘ └───────
par └──────────┘ └┘ └───────
pid ┴└──┘└┘ └┘ ┴┴└─────
st └───────────────────────────────────────────────
669 @connected_space.is_connected_univ α _ _ s t
id └───────────────────────────────┘ ┴ ┴ ┴
src ─┘ └───────────────────────────────┘┴ └───┘ ┴ └
typ ─┘ └───────────────────────────────┘┴┴└───┘┴┴┴└
doc ─┘ ┴ └───┘ ┴ └
txt ─┘ ┴ └───┘ ┴ └
par ─┘ ┴ └───┘ ┴ └
pid ─┘ ┴ └───┘ ┴ └
st ───────────────────────────────────────────────
670
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
671 theorem is_clopen_iff [connected_space α] {s : set α} : is_clopen s ↔ s = ∅ ∨ s = univ :=
id └─────────────┘ ┴ └─┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
src └─────────────┘ └─┘ └───────┘ ┴ ┴ ┴ ┴ ┴ └──┘
typ └─────────────┘ ┴ └─┘ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘
doc └─────────────┘ └───────┘
672 ⟨λ hs, classical.by_contradiction $ λ h,
id └┘ └────────────────────────┘ ┴
src └────────────────────────┘
typ └┘ └────────────────────────┘ ┴
673 have h1 : s ≠ ∅ ∧ -s ≠ ∅, from ⟨mt or.inl h,
id ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └┘ └────┘ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────┘
typ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ └┘ └────┘ ┴
674 mt (λ h2, or.inr $ (by rw [← compl_compl s, h2, compl_empty] : s = univ)) h⟩,
id └┘ └┘ └────┘ └─────────┘ ┴ └┘ └─────────┘ ┴ ┴ └──┘ ┴
src └┘ └────┘ └────┘└─────────┘┴ └┘ └┘└─────────┘└┘ ┴ └──┘
typ └┘ └┘ └────┘ └────┘└─────────┘┴┴└┘└┘└┘└─────────┘└┘ ┴ ┴ └──┘ ┴
doc └────┘ ┴ └┘ └┘ └┘
txt └────┘ ┴ └┘ └┘ └┘
par └────┘ ┴ └┘ └┘ └┘
pid └──┘ ┴ └┘ └┘ ┴┴
st └──────────────────┘└──┘└───────────┘┴┴
675 let ⟨_, h2, h3⟩ := exists_mem_inter hs.1 hs.2 (union_compl_self s)
id └─┘ └┘ └┘ └──────────────┘ └┘┴ └┘┴ └──────────────┘ ┴
src └──────────────┘ ┴ ┴ └──────────────┘
typ └─┘ └┘ └┘ └──────────────┘ └┘┴ └┘┴ └──────────────┘ ┴
676 (ne_empty_iff_nonempty.1 h1.1) (ne_empty_iff_nonempty.1 h1.2) in
id └───────────────────┘┴ └┘┴ └───────────────────┘┴ └┘┴
src └───────────────────┘┴ ┴ └───────────────────┘┴ ┴
typ └───────────────────┘┴ └┘┴ └───────────────────┘┴ └┘┴
677 h3 h2,
678 by rintro (rfl | rfl); [exact is_clopen_empty, exact is_clopen_univ]⟩
id ┴ └─────────────┘ └────────────┘
src └────────────────┘ ┴└────┘└─────────────┘ └────┘└────────────┘
typ └────────────────┘ ┴└────┘└─────────────┘ └────┘└────────────┘
doc └────────────────┘ └────┘ └────┘
txt └────────────────┘ └────┘ └────┘
par └────────────────┘ └────┘ └────┘
pid └──────────┘ ┴ ┴
st └────────────────────────────────────────────────────────────────┘
679
680 end connected
681
682 section totally_disconnected
683
684 /-- A set is called totally disconnected if all of its connected components are singletons. -/
685 def is_totally_disconnected (s : set α) : Prop :=
id └─┘ ┴
src └─┘
typ └─┘ ┴
686 ∀ t, t ⊆ s → is_connected t → subsingleton t
id ┴ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴
src ┴ └──────────┘ └──────────┘
typ ┴ ┴ ┴ ┴ └──────────┘ ┴ └──────────┘ ┴
doc └──────────┘
687
688 theorem is_totally_disconnected_empty : is_totally_disconnected (∅ : set α) :=
id └─────────────────────┘ ┴ └─┘ ┴
src └─────────────────────┘ ┴ └─┘
typ └─────────────────────┘ ┴ └─┘ ┴
doc └─────────────────────┘
689 λ t ht _, ⟨λ ⟨_, h⟩, (ht h).elim⟩
id ┴ └┘ ┴ ┴ ┴ └┘ └──┘
src └──┘
typ ┴ └┘ ┴ ┴ ┴ └┘ └──┘
690
691 theorem is_totally_disconnected_singleton {x} : is_totally_disconnected ({x} : set α) :=
id └─────────────────────┘ ┴┴ └─┘ ┴
src └─────────────────────┘ ┴ └─┘
typ └─────────────────────┘ ┴┴ └─┘ ┴
doc └─────────────────────┘
692 λ t ht _, ⟨λ ⟨p, hp⟩ ⟨q, hq⟩, subtype.eq $ show p = q,
id ┴ └┘ ┴ ┴┴ └┘ ┴┴ └┘ └────────┘ ┴
src └────────┘ ┴
typ ┴ └┘ ┴ ┴┴ └┘ ┴┴ └┘ └────────┘ ┴
693 from (eq_of_mem_singleton (ht hp)).symm ▸ (eq_of_mem_singleton (ht hq)).symm⟩
id └─────────────────┘ └┘ └──┘ ┴ └─────────────────┘ └┘ └──┘
src └─────────────────┘ └──┘ ┴ └─────────────────┘ └──┘
typ └─────────────────┘ └┘ └──┘ ┴ └─────────────────┘ └┘ └──┘
694
695 /-- A space is totally disconnected if all of its connected components are singletons. -/
696 class totally_disconnected_space (α : Type u) [topological_space α] : Prop :=
id └──┘ └───────────────┘ ┴
src └───────────────┘
typ └──┘ └───────────────┘ ┴
doc └───────────────┘
697 (is_totally_disconnected_univ : is_totally_disconnected (univ : set α))
id └─────────────────────┘ └──┘ └─┘ ┴
src └─────────────────────┘ └──┘ └─┘
typ └─────────────────────┘ └──┘ └─┘ ┴
doc └─────────────────────┘
698
699 end totally_disconnected
700
701 section totally_separated
702
703 /-- A set `s` is called totally separated if any two points of this set can be separated
704 by two disjoint open sets covering `s`. -/
705 def is_totally_separated (s : set α) : Prop :=
id └─┘ ┴
src └─┘
typ └─┘ ┴
706 ∀ x ∈ s, ∀ y ∈ s, x ≠ y → ∃ u v : set α, is_open u ∧ is_open v ∧
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴
src ┴ ┴ └─┘ ┴ └─────┘ ┴ └─────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴┴ └─────┘ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘ └─────┘
707 x ∈ u ∧ y ∈ v ∧ s ⊆ u ∪ v ∧ u ∩ v = ∅
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
708
709 theorem is_totally_separated_empty : is_totally_separated (∅ : set α) :=
id └──────────────────┘ ┴ └─┘ ┴
src └──────────────────┘ ┴ └─┘
typ └──────────────────┘ ┴ └─┘ ┴
doc └──────────────────┘
710 λ x, false.elim
id ┴ └────────┘
src └────────┘
typ ┴ └────────┘
711
712 theorem is_totally_separated_singleton {x} : is_totally_separated ({x} : set α) :=
id └──────────────────┘ ┴┴ └─┘ ┴
src └──────────────────┘ ┴ └─┘
typ └──────────────────┘ ┴┴ └─┘ ┴
doc └──────────────────┘
713 λ p hp q hq hpq, (hpq $ (eq_of_mem_singleton hp).symm ▸ (eq_of_mem_singleton hq).symm).elim
id ┴ └┘ ┴ └┘ └─┘ └─┘ └─────────────────┘ └┘ └──┘ ┴ └─────────────────┘ └┘ └──┘ └──┘
src └─────────────────┘ └──┘ ┴ └─────────────────┘ └──┘ └──┘
typ ┴ └┘ ┴ └┘ └─┘ └─┘ └─────────────────┘ └┘ └──┘ ┴ └─────────────────┘ └┘ └──┘ └──┘
714
715 theorem is_totally_disconnected_of_is_totally_separated {s : set α}
id └─┘ ┴
src └─┘
typ └─┘ ┴
716 (H : is_totally_separated s) : is_totally_disconnected s :=
id └──────────────────┘ ┴ └─────────────────────┘ ┴
src └──────────────────┘ └─────────────────────┘
typ └──────────────────┘ ┴ └─────────────────────┘ ┴
doc └──────────────────┘ └─────────────────────┘
717 λ t hts ht, ⟨λ ⟨x, hxt⟩ ⟨y, hyt⟩, subtype.eq $ classical.by_contradiction $
id ┴ └─┘ └┘ ┴┴ └─┘ ┴┴ └─┘ └────────┘ └────────────────────────┘
src └────────┘ └────────────────────────┘
typ ┴ └─┘ └┘ ┴┴ └─┘ ┴┴ └─┘ └────────┘ └────────────────────────┘
718 assume hxy : x ≠ y, let ⟨u, v, hu, hv, hxu, hyv, hsuv, huv⟩ := H x (hts hxt) y (hts hyt) hxy in
id ┴ └─┘ ┴ ┴ └┘ └┘ └─┘ └─┘ └──┘ └─┘ ┴ └─┘ └─┘ └─┘
src ┴
typ ┴ └─┘ ┴ ┴ └┘ └┘ └─┘ └─┘ └──┘ └─┘ ┴ └─┘ └─┘ └─┘
719 let ⟨r, hrt, hruv⟩ := ht u v hu hv (subset.trans hts hsuv) ⟨x, hxt, hxu⟩ ⟨y, hyt, hyv⟩ in
id └─┘ ┴ └──┘ └┘ └──────────┘ └─┘
src └──────────┘
typ └─┘ ┴ └──┘ └┘ └──────────┘ └─┘
720 ((ext_iff _ _).1 huv r).1 hruv⟩
id └─────┘ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴ ┴
721
722 /-- A space is totally separated if any two points can be separated by two disjoint open sets
723 covering the whole space. -/
724 class totally_separated_space (α : Type u) [topological_space α] : Prop :=
id └──┘ └───────────────┘ ┴
src └───────────────┘
typ └──┘ └───────────────┘ ┴
doc └───────────────┘
725 (is_totally_separated_univ : is_totally_separated (univ : set α))
id └──────────────────┘ └──┘ └─┘ ┴
src └──────────────────┘ └──┘ └─┘
typ └──────────────────┘ └──┘ └─┘ ┴
doc └──────────────────┘
726
727 @[priority 100] -- see Note [lower instance priority]
728 instance totally_separated_space.totally_disconnected_space (α : Type u) [topological_space α]
id └───────────────┘ ┴
src └───────────────┘
typ └───────────────┘ ┴
doc └───────────────┘
729 [totally_separated_space α] : totally_disconnected_space α :=
id └─────────────────────┘ ┴ └────────────────────────┘ ┴
src └─────────────────────┘ └────────────────────────┘
typ └─────────────────────┘ ┴ └────────────────────────┘ ┴
doc └─────────────────────┘ └────────────────────────┘
730 ⟨is_totally_disconnected_of_is_totally_separated $ totally_separated_space.is_totally_separated_univ α⟩
id └─────────────────────────────────────────────┘ └───────────────────────────────────────────────┘ ┴
src └─────────────────────────────────────────────┘ └───────────────────────────────────────────────┘
typ └─────────────────────────────────────────────┘ └───────────────────────────────────────────────┘ ┴
731
732 end totally_separated